From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 11096 invoked from network); 16 Mar 2023 12:38:46 -0000 Received: from mail-qt1-x83c.google.com (2607:f8b0:4864:20::83c) by inbox.vuxu.org with ESMTPUTF8; 16 Mar 2023 12:38:46 -0000 Received: by mail-qt1-x83c.google.com with SMTP id c5-20020ac84e05000000b003d6a808a388sf774140qtw.8 for ; Thu, 16 Mar 2023 05:38:46 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; t=1678970325; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:message-id:to:from:date:sender:from:to:cc:subject:date :message-id:reply-to; bh=6takdy1A437iO0Zw7DiLcuLs4DWQE/eT9nIpAHzR/8o=; b=NCP3MKpl7VA6jhNcnBinVSF06Q6MWMgoY9BmcFZ0WPQcr2cr30grW7Ckin7AqZ1Oqb wJTtmz5za/We3OYo3sAr1kwogG0SuzV0AV+RXBpLJ//tsRdKjUKbjVLWwbjEhqw/4igF dh70/EW5ExjdA/HGczZnWkNo4wEsd+eXN2pc3XVwjz3hkuoOdlGvZSamUjROVE+IWUjF X6AHDPJY1+TvJOvLuVxWbAZoCQDYOOudIuDR2vuwFBelKvTs1iOobyVKtWggxIaox4ik MypLFn+7qvLcI9tgEjf3nTN/xnwqiQOgJbuSKMIctf5eqCT3gyWXipm5yhkwHU6fFfsM +XQA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; t=1678970325; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-sender:mime-version :subject:message-id:to:from:date:from:to:cc:subject:date:message-id :reply-to; bh=6takdy1A437iO0Zw7DiLcuLs4DWQE/eT9nIpAHzR/8o=; b=jnBUCpry4taZ6Bc8nklv0A1Ry1zYYE8SbA4QoT/aE/6J6kyneRPeZSL9wnuk8PW1Y8 Kznb/21TohRKX0J5bkCPa1YvWjVTdOf4+5Thtyp30WZwWe6Nk8SaZEH5Ar/nGJd+ZYxj MQD5KWCW/2tGddYaXFInS++B+dK4X4X+3WAWEdFMYSFcQqoSg94romD0d827UsxZ0YgX go5OF4EpZtPgnsDgQCHMMGobYxHcsjJFsfSCcT0qMJ3wq2kE1AhUpQB3mhnIpDBDv8DL aHjr/GGMT9NmTVhkhijoUdSkS4Hfp+aoqsLFfAkUpt7SrJS8aolk/82rTbRjZ+APy1XG L8mQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; t=1678970325; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-sender:mime-version:subject:message-id:to:from:date :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to; bh=6takdy1A437iO0Zw7DiLcuLs4DWQE/eT9nIpAHzR/8o=; b=SiF8hrTxK+R9eSIjwmknIxHdMGASYMC6rT83P5BLVEDl3694fx69ptytPz8jLL8kg0 JKkIQco9x0c6KTqIeoUlfWctIfIkL1a+nz3ELtL4txMIeZs+dk0hgSl02Jv8yAHQtvaz wThInjKwgWGsYINn2VEoPEKjPU25JTK2vmeX00KwDUY3wjzlOH4HOG3YJ0g92xZ4VMGi DeNBFftaJjiDG5pxe+vg1Jfe3/3qLeGQ3T96afPB+Nueq2/AYXfeRqJtXCA7oK1V85+Z bxg6Wu5lOx8iDhaYqK8o4AQssMTvPDn985zmjawU3HajOFUGqdDDIuVMRYfWteYiY4lu lbMA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AO0yUKWPl2+q7aDh5LjDnwwlW2kj8jPVx7ttIW4b+V6NsPE0OSSnkn4f 44VGqKSQjB+GdPioxHBvV3U= X-Google-Smtp-Source: AK7set/B2ywB9fwz4SOcqZP/YHKGDj9QGF3b7OtXGEqALbREtcB1ICrgM/HVNwsEuAd4Tn8e57ue1w== X-Received: by 2002:ac8:7d01:0:b0:3d8:2cb6:d21d with SMTP id g1-20020ac87d01000000b003d82cb6d21dmr394200qtb.6.1678970325489; Thu, 16 Mar 2023 05:38:45 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:620a:2728:b0:746:224a:4cad with SMTP id b40-20020a05620a272800b00746224a4cadls366599qkp.0.-pod-prod-gmail; Thu, 16 Mar 2023 05:38:44 -0700 (PDT) X-Received: by 2002:a05:620a:1190:b0:743:7dcc:282a with SMTP id b16-20020a05620a119000b007437dcc282amr5471445qkk.8.1678970323874; Thu, 16 Mar 2023 05:38:43 -0700 (PDT) Date: Thu, 16 Mar 2023 05:38:43 -0700 (PDT) From: "mathie...@gmail.com" To: Homotopy Type Theory Message-Id: Subject: =?UTF-8?Q?=5BHoTT=5D_=5BCMU=2DHoTT=5D_Special_series_of_lectures_=E2=80=94_Cis?= =?UTF-8?Q?inski=2C_Nguyen=2C_Walde_on_=2AUnivalent_Directed_Type_Theory=2A?= MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1288_1742019130.1678970323010" X-Original-Sender: mathieu.anel@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , ------=_Part_1288_1742019130.1678970323010 Content-Type: multipart/alternative; boundary="----=_Part_1289_80498678.1678970323010" ------=_Part_1289_80498678.1678970323010 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable ~*~*~*~*~*~*~*~* CMU HoTT Seminar Online *~*~*~*~*~*~*~*~ The CMU team is happy to invite all of you for a special series of three=20 lectures by Denis-Charles Cisinski (Universit=C3=A4t Regensburg) Hoang Kim Nguyen (Universit=C3=A4t Regensburg) Tashi Walde (Technische Universit=C3=A4t M=C3=BCnchen) on *** Univalent Directed Type Theory *** (abstract below) Lecture 1 =E2=80=94 video , = slides=20 intro=20 , slides talk=20 Next lectures Lecture 2 =E2=80=94 *Monday March 20*(10am-12pm EDT / 3pm-5pm CET) Lecture 3 =E2=80=94 Monday March 27 (10am-12pm EDT / 4pm-6pm CEST) Beware the time difference USA/Europe (EDT/CET) is only 5h for the 13 &=20 20th but 6h for the 27th (EDT/CEST) Abstract: We will introduce a version of dependent type theory that is suitable to=20 develop a synthetic theory of 1=E2=80=91categories. The axioms are both a f= ragment=20 and an extension of ordinary dependent type theory. The axioms are chosen= =20 so that (=E2=88=9E,1)=E2=80=91category theory (under the form of quasi-cate= gories or=20 complete Segal spaces) gives a semantic interpretation, in a way which=20 extends Voevodsky's interpretation of univalent dependent type theory in=20 the homotopy theory of Kan complexes. More generally, using a slight=20 generalization of Shulman's methods, we should be able to see that the=20 theory of (=E2=88=9E,1)=E2=80=91categories internally in any =E2=88=9E=E2= =80=91topos (as developed by=20 Martini and Wolf) is a semantic interpretation as well (hence so is=20 parametrized higher category theory introduced by Barwick, Dotto, Glasman,= =20 Nardin and Shah). There are of course strong links with =E2=88=9E=E2=80=91c= osmoi of Riehl=20 and Verity as well as with cubical Hott (as strongly suggested by the work= =20 of Licata and Weaver), or simplicial Hott (as in the work of Buchholtz and= =20 Weinberger). We will explain the axioms in detail and have a glimpse at=20 basic theorems and constructions in this context (Yoneda Lemma, Kan=20 extensions, Localizations). We will also discuss the perspective of=20 reflexivity: since the theory speaks of itself (through directed=20 univalence), we can use it to justify new deduction rules that express the= =20 idea of working up to equivalence natively (e.g. we can produce a logic by= =20 rectifying the idea of having a locally cartesian type). In particular,=20 this logic can be used to produce and study semantic interpretations of=20 Hott. Link for the Zoom Meeting https://cmu.zoom.us/j/622894049?pwd=3DbkhtRlNxL3E3SnZCTU1oSFNHcHJNQT09 Meeting ID: 622 894 049 Passcode: =E2=80=98the Brunerie number=E2=80=99 Seminar webpage https://www.cmu.edu/dietrich/philosophy/hott/seminars/index.html#230313 --=20 You received this message because you are subscribed to the Google Groups "= Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/c864a21a-ba63-4e34-b174-e683d9afd132n%40googlegroups.com= . ------=_Part_1289_80498678.1678970323010 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

~*~*~*~*~*~*~*~* CMU HoTT = Seminar Online *~*~*~*~*~*~*~*~


The CMU team is happy to invite all of you for a special series = of three lectures by


= Denis-Charles Cisinski (Universit=C3=A4t Regensburg)

Hoang Kim Nguyen (Universit=C3=A4t Regensburg= )

Tashi Walde (Technisc= he Universit=C3=A4t M=C3=BCnchen)


on=C2=A0** Univalent Directed Type Theory **

(abstract below)


Lecture 1 =E2=80=94=C2= =A0video,=C2=A0slides intro,=C2=A0slid= es talk


Next lectures

Lecture 3 =E2=80=94= Monday March 27 (10am-12pm EDT / 4pm-6pm CEST)


Beware the time difference USA/Europe (EDT/CET) = is only 5h for the 13 & 20th but 6h for the 27th (EDT/CEST)



Abstract:


We will introduce a version of dependent = type theory that is suitable to develop a synthetic theory of 1=E2=80=91cat= egories. The axioms are both a fragment and an extension of ordinary depend= ent type theory. The axioms are chosen so that (=E2=88=9E,1)=E2=80=91catego= ry theory (under the form of quasi-categories or complete Segal spaces) giv= es a semantic interpretation, in a way which extends Voevodsky's interpreta= tion of univalent dependent type theory in the homotopy theory of Kan compl= exes. More generally, using a slight generalization of Shulman's methods, w= e should be able to see that the theory of (=E2=88=9E,1)=E2=80=91categories= internally in any =E2=88=9E=E2=80=91topos (as developed by Martini and Wol= f) is a semantic interpretation as well (hence so is parametrized higher ca= tegory theory introduced by Barwick, Dotto, Glasman, Nardin and Shah). Ther= e are of course strong links with =E2=88=9E=E2=80=91cosmoi of Riehl and Ver= ity as well as with cubical Hott (as strongly suggested by the work of Lica= ta and Weaver), or simplicial Hott (as in the work of Buchholtz and Weinber= ger). We will explain the axioms in detail and have a glimpse at basic theo= rems and constructions in this context (Yoneda Lemma, Kan extensions, Local= izations). We will also discuss the perspective of reflexivity: since the t= heory speaks of itself (through directed univalence), we can use it to just= ify new deduction rules that express the idea of working up to equivalence = natively (e.g. we can produce a logic by rectifying the idea of having a lo= cally cartesian type). In particular, this logic can be used to produce and= study semantic interpretations of Hott.



Link for the Zoom Meeting

https://cmu.zoom.us/j/622894049?pwd=3DbkhtRlNxL3E3SnZCTU1oSFNHcHJNQ= T09

Meeting = ID: 622 894 049

Passcod= e: =E2=80=98the Brunerie number=E2=80=99


Seminar webpage

https://www.cmu.edu/dietrich/philosophy/hott/semin= ars/index.html#230313


--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.c= om/d/msgid/HomotopyTypeTheory/c864a21a-ba63-4e34-b174-e683d9afd132n%40googl= egroups.com.
------=_Part_1289_80498678.1678970323010-- ------=_Part_1288_1742019130.1678970323010--