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 14260 invoked from network); 23 Mar 2023 18:00:55 -0000 Received: from mail-wr1-x437.google.com (2a00:1450:4864:20::437) by inbox.vuxu.org with ESMTPUTF8; 23 Mar 2023 18:00:55 -0000 Received: by mail-wr1-x437.google.com with SMTP id k16-20020adfd230000000b002cfe7555486sf2696945wrh.13 for ; Thu, 23 Mar 2023 11:00:55 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1679594454; cv=pass; d=google.com; s=arc-20160816; b=LIGcCo6pf/OZlqz1xui5tAR6cof4OUnYASwxWeKqvYIdiZExJFEMFEMwr39mOPrhsk DqCvV4O+/51BdAlxHAGiJhvrP6hm9JUycnCmK2m1NRc51xiaRp611iDkKu+HLDvtqfyB fqCj8qE3xE00SR1z79kELT8KVn27/LB5Vd7qD2X33TDzuM3iJzf+SDcurCUh7cDGdXCx Q1SWBO6zBUCzOL1JuiLbN0hdoyXmd+s6OGswjRZ9flQU7R4eBmiPXWbfb9+cSXo4+gdS aJwa/JgwCEyabocpsZcuCA7I4rL21gfgA2juFqTXCN7ILgpb1MY0TQsuwXmo3AKl6evg Ecog== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:to:subject:message-id:date:from :mime-version:sender:dkim-signature:dkim-signature; bh=KQlZFM4Y/At/PlUvKaEOICTGDBpi51JAGyradBW8Szg=; b=W6/9TeGF8aCP3vjYImKrgH9ICg3/zRuoS5n4Kw73o2YoQ36EVWUjbWtBGGbkDtrFHL 67VQg7PvZQjoS4Wqvooqr/AJ3Qol7xuhYhRAqde8NzC4CktcsddEHsRuGykH4DxIKDcP EDMZrdGkgotfKp/21IvhKGCYWoRlXZ4pvIpBGHXSD0j6Qw1660B6Ue/dGDZ/n3F157jk n988BIMyZrhasn9GEvR8Oy+NQwfYgrQnDL5ci8iEa+O/8FoCxCzyLHFzWcsk2B32gQFs oO4d/qUOQRNobTN5OeGhnquYmFlgi2vYYONnnWueBBYeVK7kwjsrcRU48dkIOu1Q/UB0 JaGA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=Wf4kaMK6; spf=pass (google.com: domain of mathieu.anel@gmail.com designates 2a00:1450:4864:20::52d as permitted sender) smtp.mailfrom=mathieu.anel@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; t=1679594454; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:to:subject:message-id:date:from:mime-version :sender:from:to:cc:subject:date:message-id:reply-to; bh=KQlZFM4Y/At/PlUvKaEOICTGDBpi51JAGyradBW8Szg=; b=aVEOsnb8NbTnercQASsxfUSAkyl2B0I2WhjwpZJpgzFrz1v1c70hGVL3X2t6URsrDf vSecNHMHz7jJ2DIw5xE+dcLV/gijt3nGWytJ9ZH2aM4ldi+eaEAbRl0127qHH7ZB1ZdM dQCdsC7+ltP24B0yIFd7ltooxhnGPsrp9eCsq4NwYU/2JI6yQFW08Cv5jlS/9wHGAAc7 KxytPkiUt+p+5Xwuhb/T1BbXujkcZJg8ufGMqzOMbr0CBUXxd4k2/X1F9ZtH/OVKJXuS 9FkCEa/Rz0qsECkBs0hghyFLJOJPPDdjN/Zb3teVlx+PPVpRiXPDaSnzWPROLAeZk5e8 l7yg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; t=1679594454; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:to:subject:message-id:date:from:mime-version:from :to:cc:subject:date:message-id:reply-to; bh=KQlZFM4Y/At/PlUvKaEOICTGDBpi51JAGyradBW8Szg=; b=aeeXYCTS15+3Wm5Tp1cYcmU9Ym5OIc3ZHlW8Gjp5E9vhxGDGZ1/VabsVW5fBBEpZJ/ dfw4plTCjnrf+i1v4UU/RFVQcqXQSVUxAK7xrXONnCq4XTDAWxkhY4dvX/GRBGZjDvE6 7D1nFmDtisN5N/OXaQViyDRG/HSShgd5K4WkkxwqzegqP4o2uktjekCjKdQf8GyQ/mwr 1oIszvYILnkwXTkf+O8lnc4d0uUH80eimtqziQ5R5afOehAPWBpU4CG0syk/1uzWdzT2 XJT7i5yyP81omS4v1RiikYtHi/+VpOTtRaWikEkvsbZRwqxgwaMJdEfUQYACMAHxnImd 41FQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; t=1679594454; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:to:subject :message-id:date:from:mime-version:x-gm-message-state:sender:from:to :cc:subject:date:message-id:reply-to; bh=KQlZFM4Y/At/PlUvKaEOICTGDBpi51JAGyradBW8Szg=; b=nbI6A+l79DevdW0WaQuSU6zzf3UleMwMkie+jipwM4tYkKbtN615BG9osFKnDEBK7C 1q1gtuU7F+TZwKn2uIS9GpZyGDgO7/H6KiqL4l+WcMIqAjp1gmHiAVsrWfZ+8BFKDf18 ozINraRUlDPH/ngAWRWluY77sfaenfYQxlUpbqiwg1UJpJfWpGCEqCh8lTIPNX3iujfJ lcfVy7fde6hT/9ATUmlkE24BnhVyEtgEHo34h1Bns/2CHfoDFQYrWYW9vHaF3ZfNNjdb 8mxEw1bq0BvfGegh0stqyz4+8ydN+EpjPn8+lhiovl9quKFv/a25owQhir86zhyWF7EY Ek7g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AAQBX9cmRyjC+0l5CiYsIF/I6jBxRFArY/K2lSjtJ5ZAJX+neDVOF2mv ZFRX0SdMLXfStiKVIBOMTYU= X-Google-Smtp-Source: AKy350YV24iI0Rsl3IwkmANADcsp184/GtDAeJ9z+FxrWACxyuwpAOvfuJfHwRnKd82OaeCGK0laLA== X-Received: by 2002:a5d:6b0a:0:b0:2d1:cc54:11ba with SMTP id v10-20020a5d6b0a000000b002d1cc5411bamr8290wrw.11.1679594453796; Thu, 23 Mar 2023 11:00:53 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6000:3ce:b0:2d0:a74b:1d65 with SMTP id b14-20020a05600003ce00b002d0a74b1d65ls7594726wrg.1.-pod-prod-gmail; Thu, 23 Mar 2023 11:00:51 -0700 (PDT) X-Received: by 2002:adf:d08a:0:b0:2d4:99f:6701 with SMTP id y10-20020adfd08a000000b002d4099f6701mr23716wrh.58.1679594451280; Thu, 23 Mar 2023 11:00:51 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1679594451; cv=none; d=google.com; s=arc-20160816; b=JzsNn1ZDEu/ZufTDY7MwH9jJ9Mqf8MW1BUbauvGSKdPTgS/7NLzqGIh2fyxOe/NxH1 hNmyW3Qs3QcuMDDHy79yCSCaNDOvHmUT8zoN8hYePvU/pm5NZZUhYJOTHoPNHXdfZCBj l1+GaiQTjP+SCuANDqMSBEwCmNpLSccK+D1E7FnbltP8wv26hac9pBFoheRT3sde9I3B As3EVnqK+AWPMsuyaMIlEvlM97E8NKZ5RMQ3wGC/LvIgFO2Tc39S5opclVHEIC48vOa/ UxOOyP1vXVey6PrElsTnZ49C5pgX1S50d1MCZ65Iu27nl/Nxraj/qKhhdn1Un6cAtfno qqNw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=4K3+Kp8zhuU7LurbwGoI50aUYwkxsSSFYshbCjQwTkA=; b=FprzNKqjbmuZtWhsgNerbDHybz5F3Rm6BfA1fD8v1T9MxWRbEOK066+m8fTxRSi4Yg di+h6lEPCR8GMcRDrwjMQckv7S1xeObh0Qxm91wPMYayU6C+8SJEVBfLGR70QxRaCtti Mksa3zji0UegS79PNr0Hbpvh4VMszldN6d5LUUvahY1K1s3qf3kXba+IsNivbQ8w7yMc TAzgIZA2wTSXf4amhsoNzQSa6/PuFz7STwC+M/eo6N5mk8/bi55baNVsyiQxz/ijL9Xr UcrZU0+/iaKowfWgrHVfP+tVBdQJZ9oFv2D9S4EEsn2Rd3EdIah0d15/qhEm8YrG3+LI 7c5Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=Wf4kaMK6; spf=pass (google.com: domain of mathieu.anel@gmail.com designates 2a00:1450:4864:20::52d as permitted sender) smtp.mailfrom=mathieu.anel@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ed1-x52d.google.com (mail-ed1-x52d.google.com. [2a00:1450:4864:20::52d]) by gmr-mx.google.com with ESMTPS id bp11-20020a5d5a8b000000b002c6e883154bsi813790wrb.1.2023.03.23.11.00.51 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 23 Mar 2023 11:00:51 -0700 (PDT) Received-SPF: pass (google.com: domain of mathieu.anel@gmail.com designates 2a00:1450:4864:20::52d as permitted sender) client-ip=2a00:1450:4864:20::52d; Received: by mail-ed1-x52d.google.com with SMTP id eg48so90272328edb.13 for ; Thu, 23 Mar 2023 11:00:51 -0700 (PDT) X-Received: by 2002:a50:9f6f:0:b0:4fb:2593:846 with SMTP id b102-20020a509f6f000000b004fb25930846mr147422edf.3.1679594450758; Thu, 23 Mar 2023 11:00:50 -0700 (PDT) MIME-Version: 1.0 From: mathieu anel Date: Thu, 23 Mar 2023 14:00:39 -0400 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?= To: homotopytypetheory@googlegroups.com Content-Type: multipart/alternative; boundary="0000000000009ab08805f7950e22" X-Original-Sender: mathieu.anel@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=Wf4kaMK6; spf=pass (google.com: domain of mathieu.anel@gmail.com designates 2a00:1450:4864:20::52d as permitted sender) smtp.mailfrom=mathieu.anel@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , --0000000000009ab08805f7950e22 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable ~*~*~*~*~*~*~*~* CMU HoTT Seminar Online *~*~*~*~*~*~*~*~ Don't miss lecture 3 ! 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 https://www.youtube.com/watch?v=3D5YOltuTcBK8 Slides intro https://www.cmu.edu/dietrich/philosophy/hott/seminars/slides/cisinski-nguye= n-walde-intro_talk1.pdf Slides talk https://www.cmu.edu/dietrich/philosophy/hott/seminars/slides/cisinski-nguye= n-walde-talk1.pdf Lecture 2 =E2=80=94 video https://www.youtube.com/watch?v=3DxWmELBvHMPo Slides https://www.cmu.edu/dietrich/philosophy/hott/seminars/slides/cisinski-nguye= n-walde-talk2.pdf *Next lecture* *Lecture 3 =E2=80=94 Monday March 27 (10am-12pm EDT / 4pm-6pm CEST)* Abstract: We will introduce a version of dependent type theory that is suitable to develop a synthetic theory of 1=E2=80=91categories. The axioms are both a f= ragment and an extension of ordinary dependent type theory. The axioms are chosen so that (=E2=88=9E,1)=E2=80=91category theory (under the form of quasi-cate= gories or complete Segal spaces) gives a semantic interpretation, in a way which extends Voevodsky's interpretation of univalent dependent type theory in the homotopy theory of Kan complexes. More generally, using a slight generalization of Shulman's methods, we 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 Wolf) is a semantic interpretation as well (hence so is parametrized higher category theory introduced by Barwick, Dotto, Glasman, Nardin and Shah). There are of course strong links with =E2=88=9E=E2=80=91c= osmoi of Riehl and Verity as well as with cubical Hott (as strongly suggested by the work of Licata and Weaver), or simplicial Hott (as in the work of Buchholtz and Weinberger). We will explain the axioms in detail and have a glimpse at basic theorems and constructions in this context (Yoneda Lemma, Kan extensions, Localizations). We will also discuss the perspective of reflexivity: since the theory speaks of itself (through directed univalence), we can use it to justify 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 locally 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=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/CAD3N2UZznZkfh6rZTzg9YhP0gYiOfiq7gEVn78P-S99Yo1wXQw%40ma= il.gmail.com. --0000000000009ab08805f7950e22 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


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


Don't miss lecture 3 !


Denis-Charles Cisinski (Universit=C3=A4t Regensb= urg)

Hoang Ki= m Nguyen (Universit=C3=A4t Regensburg)

Tashi Walde (Technische Universit=C3=A4t M=C3=BCn= chen)


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

(abstract below)


Lecture 1= =E2=80=94 video=C2=A0https://www.youtub= e.com/watch?v=3D5YOltuTcBK8

Slides intr= o=C2=A0https://www.cmu.edu/dietrich/philosophy/hott/seminars/s= lides/cisinski-nguyen-walde-intro_talk1.pdf

Slides talk=C2=A0https://www.cmu.edu/dietrich/philosophy/hott/s= eminars/slides/cisinski-nguyen-walde-talk1.pdf


Lecture 2 =E2=80=94 video=C2=A0https://www.youtube.com/watch?v=3DxWmELBvHMPo

Slides=C2=A0https://www.cmu.edu/dietrich/philosophy/ho= tt/seminars/slides/cisinski-nguyen-walde-talk2.pdf


=

Next lecture<= /b>

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



Abstrac= t:


We= will introduce a version of dependent type theory that is suitable to deve= lop a synthetic theory of 1=E2=80=91categories. The axioms are both a fragm= ent and an extension of ordinary dependent type theory. The axioms are chos= en so that (=E2=88=9E,1)=E2=80=91category theory (under the form of quasi-c= ategories or complete Segal spaces) gives a semantic interpretation, in a w= ay which extends Voevodsky's interpretation of univalent dependent type= theory in the homotopy theory of Kan complexes. More generally, using a sl= ight generalization of Shulman's methods, we 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 Wolf) is a semantic interpretat= ion as well (hence so is parametrized higher category theory introduced by = Barwick, Dotto, Glasman, Nardin and Shah). There are of course strong links= with =E2=88=9E=E2=80=91cosmoi of Riehl and Verity as well as with cubical = Hott (as strongly suggested by the work of Licata and Weaver), or simplicia= l Hott (as in the work of Buchholtz and Weinberger). We will explain the ax= ioms in detail and have a glimpse at basic theorems and constructions in th= is context (Yoneda Lemma, Kan extensions, Localizations). We will also disc= uss the perspective of reflexivity: since the theory speaks of itself (thro= ugh directed univalence), we can use it to justify new deduction rules that= express the idea of working up to equivalence natively (e.g. we can produc= e a logic by rectifying the idea of having a locally cartesian type). In pa= rticular, this logic can be used to produce and study semantic interpretati= ons of Hott.



Link for the Zoom Meeting

https://cmu.zoom.us/j/622894049?pwd=3DbkhtRlNxL3E3SnZCTU1oS= FNHcHJNQT09

Meeting ID: 622 894 049

Passcode: =E2=80=98the Brunerie number=E2=80=99

Seminar web= page

https://www.cmu.edu/dietrich/philosophy/hott/seminars/index.html#230= 313


--
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://gro= ups.google.com/d/msgid/HomotopyTypeTheory/CAD3N2UZznZkfh6rZTzg9YhP0gYiOfiq7= gEVn78P-S99Yo1wXQw%40mail.gmail.com.
--0000000000009ab08805f7950e22--