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 22520 invoked from network); 2 Mar 2023 18:40:54 -0000 Received: from mail-lj1-x23f.google.com (2a00:1450:4864:20::23f) by inbox.vuxu.org with ESMTPUTF8; 2 Mar 2023 18:40:54 -0000 Received: by mail-lj1-x23f.google.com with SMTP id b30-20020a05651c0b1e00b002959c2fb94fsf5562993ljr.20 for ; Thu, 02 Mar 2023 10:40:54 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1677782452; cv=pass; d=google.com; s=arc-20160816; b=vmSmkWfNP9pdYN2dnfLxt+ljvbHDvOi00qPCHp4ewgmAjrFFnmlLNmPvaR9OrFKCY9 hKg80wtldbYqa06JGjYa5nlWJz4KPiY36sAQdZbG9MBDDGJCLZXxKhL6KeY+4ZuVEt8G zTh+L9yPUZeohw/Nn/YUad833BjJYmDchpnEelHb4tNcH8gWBJpzBDqGYs/9XKeMc1Ma dIQZQ9zPcjkD/zKCKhtthH48Ye4/STbyO+cDIn4XviGKquJdpj3tRIXhIX42aElUoJJM Bru5Rrk5W1yXMHLneTBc4fldDKoNJpPjgg67kYi+LFjFHKin6vBG7z62brm14quBLwMs dPhw== 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:cc:to:subject:message-id:date:from :mime-version:sender:dkim-signature:dkim-signature; bh=8XPqH89bS0ya+L0qtT+QaXzlIpS2oLpomnptQ0GhV+A=; b=yaVGwjc4U9dWbldpT8S/tJGuJNBRRgjLPXj276ZyhRuWYyPk8iKU6wLjHZqHvxqGKI 9I6kGDT3qVkDf3yNq/2PLnXxypoqy5+MiJlYt36jd7oM7mGsOHTcQQSjo5Q1MlByKeIb goXrT/BIBBfshu/7rr8/JGjhT3b/TsPgHAJapLi+GLsziDr0M50G00yHdMtbvfKBcWtn aQ+yOwUMxXLk6IfnrHPXnMmF/0yPc5CD5I6Wn8PK4QEIfdh6ckBgQ8IUHr7RQFTPXflV pVAGCuFCXE/Uh6Bb96aQ8v1NbO7EGksSPkO1nF8Z+/0LoIHf+mhQKK3pJbx1fRwxRV5r 3Ouw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=difu1QiU; spf=pass (google.com: domain of mathieu.anel@gmail.com designates 2a00:1450:4864:20::52c 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; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:cc:to:subject:message-id:date:from:mime-version :sender:from:to:cc:subject:date:message-id:reply-to; bh=8XPqH89bS0ya+L0qtT+QaXzlIpS2oLpomnptQ0GhV+A=; b=RYFn4W9250S1BUETkwIimEXSxbxavXMqFCpZ1uDj/+n/nfzsHief8R4Y/BgqFzU2i0 LsD4mGIOdErQI7akaVpDWeCVXpL7XpfcTbEWa6ocaHkJo3rQj8+5MrMNm+TpIyz780pJ Wp+ftpo80HhNuHCs5QWcE40wnpuPuvBjiCHKmvz3kdZBwi3t5cNNi66YnTIxiePJORNv UyJUF4CZ9cCq6MT6l9ZE8JFtWafkFW8pLZVWn3dpLxZpwTHDAuflKqx6fb3wBX+7QaP0 n95x+jwTNg78t6kXizY7d7DcGqGVqgIUerLhxjPm3mB34wzGqiauyHv/7EixWht/PCbq SNtw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:cc:to:subject:message-id:date:from:mime-version :from:to:cc:subject:date:message-id:reply-to; bh=8XPqH89bS0ya+L0qtT+QaXzlIpS2oLpomnptQ0GhV+A=; b=iB9ZxSf8rTecjHRfSRra8a/ePwPLgQJP74lUO/hcWafxdKfsgBDoqjoGBYF1hN1CXN 2A4mdr65zAi3FzP3hBhInXkunvs1xNWkjBa0aD0W2VeCJh0/aW2xSxLSxLWhylP8Y3iD eJML5U0KeNoq4Kh+aySYjzkzv8j9wnAosbIhhadRCGSlHAIOqQR/lbSm2y8vcI0U3/jc o7xB7V3uEirHPKYi3UtVBGiilqFBwobqBLlUmVG7Fn7B01BUcfykMxCQpgmTEEaMFaz0 AEoxK2yPEH1WxZomVq1rauTgDkXj5XGf8ktrGD+EjXQ1k4m9/5F8SPOoNKYjtEqiOqzp Nw3w== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; 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:cc:to:subject :message-id:date:from:mime-version:x-gm-message-state:sender:from:to :cc:subject:date:message-id:reply-to; bh=8XPqH89bS0ya+L0qtT+QaXzlIpS2oLpomnptQ0GhV+A=; b=3dHdZm2oc7c8h8KJxBs4ETVt7jn8Qog4E/1uBcyLA8ja+pjIlpwV3TfivxpxTdNDXj eov5Pwe0wJgyS/8Qz/0L7RnloRWstyoNFomwO+ez6nwai6CkKCbGo40SrLOLas3eITb1 Hx0O/OW0p3WH8Bo4vOuFoJoxFwbYWPUSTqIBCiemBwvifvUymN6OqlDPbvHVLoOa7fkE IQNRdNMUnVmc3chIYjpXED9HeRc2+EfIDGgZ0gH29/SoHQ8jpv6Mm4GGI/QfjsZIImHc R1s1/J1P42zIUQ8iRDnz4TlOJ63FoDeGjMhIGMz9RizARnHYEwGKbUTr+XL68bxqelmc KEXQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AO0yUKWo8879fbUYLkgPRyiBA+SWhPGA3z71X4m8UgdSbJPDByTNR6JU gABdcsGNjfDKYWWvW3xxEDU= X-Google-Smtp-Source: AK7set+c5OyLcHxwWHnlfAIkJJPjCdM1mUgro95G0lLthHT7ZMYh0kfqhW6Gpk+f8SpyKVt+U5SKYg== X-Received: by 2002:ac2:5451:0:b0:4d5:ca32:6ae4 with SMTP id d17-20020ac25451000000b004d5ca326ae4mr3338520lfn.4.1677782452306; Thu, 02 Mar 2023 10:40:52 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6512:15a2:b0:4dd:8403:13fe with SMTP id bp34-20020a05651215a200b004dd840313fels550613lfb.3.-pod-prod-gmail; Thu, 02 Mar 2023 10:40:49 -0800 (PST) X-Received: by 2002:a05:6512:143:b0:4e7:4a3c:697 with SMTP id m3-20020a056512014300b004e74a3c0697mr124121lfo.38.1677782449327; Thu, 02 Mar 2023 10:40:49 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1677782449; cv=none; d=google.com; s=arc-20160816; b=SZHlEBRMZ2EbfnbIaHTmAEjnNScTDsjmdV6mTF+zE20txZVIfLALk72Tb2Dc5X7W1c Jlc+HK7At/AjXtCfzH6ZREBPunMGUTLNJ+Rm1crpZkAMcDk2NH0pyz/dTymI4hjK6BWS Qd/ePjERlAgjmctgvP9+aoleZiidpQxA9bEg0y0X/ckSTlmRTjsflgLBS5kA/pYqQQ19 3Ri9cyyZxmBtxTd58a3rIdVg1/teTD+75aHJHz0WHyN+3Q0wpfXLvxmeCx0CkTSFFaGH hqCnKCneUE5asMBfSsZaRN3YJTNRk4UDSNkL8AwK5zyCiEDVFwO0pHAyg2mF9gST4jaB hlxg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:mime-version:dkim-signature; bh=SDxEuYNNrRXbmfYdYV1zDNDnidgGr2B1TvVCEPxDCTk=; b=t//t6ooLO2cFWWOUWSnxQwcbxH0N3Gt2H9EDZxRAcLTfYG2iRewUDFg+TwfWJZP350 ET1i6UaenvtIwiRJpO63E5W2JXQ8jn2qsGNvfJ0v2TMguNBXBhhoWqiuj7Q6jeuGp5oH tSvrhzgGwQdpVrl3f+AM3iXMUDsD+Nu+qJ+lTqH1bC0jPgMypureAmw03CDO0JZENUs5 Nb5nh8tlFct1VB7eGbI20Kh3Y5EBM7qzvD1RlCVhGwCMiHPrnMwKH8kZDDfyFaHCt1Dv KncsDPVsdZNlQC7ncUerwhKQPaSn8HQQw2U7BzEJdz/Wrr0O0WAOHs3T5qJau1Zk+kvF znTA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=difu1QiU; spf=pass (google.com: domain of mathieu.anel@gmail.com designates 2a00:1450:4864:20::52c 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-x52c.google.com (mail-ed1-x52c.google.com. [2a00:1450:4864:20::52c]) by gmr-mx.google.com with ESMTPS id f20-20020ac25334000000b004dd7665b536si12921lfh.1.2023.03.02.10.40.49 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 02 Mar 2023 10:40:49 -0800 (PST) Received-SPF: pass (google.com: domain of mathieu.anel@gmail.com designates 2a00:1450:4864:20::52c as permitted sender) client-ip=2a00:1450:4864:20::52c; Received: by mail-ed1-x52c.google.com with SMTP id i34so816889eda.7; Thu, 02 Mar 2023 10:40:49 -0800 (PST) X-Received: by 2002:a50:bb69:0:b0:4af:601d:ad1 with SMTP id y96-20020a50bb69000000b004af601d0ad1mr6564500ede.0.1677782448900; Thu, 02 Mar 2023 10:40:48 -0800 (PST) MIME-Version: 1.0 From: mathieu anel Date: Thu, 2 Mar 2023 13:40:37 -0500 Message-ID: Subject: =?UTF-8?Q?=5BHoTT=5D_Special_series_of_lectures_=E2=80=94_Cisinski=2C_Nguy?= =?UTF-8?Q?en=2C_Walde_on_=2AUnivalent_Directed_Type_Theory=2A?= To: homotopytypetheory@googlegroups.com, cmu-hott@googlegroups.com Cc: Denis-Charles Cisinski , hoang-kim.nguyen@mathematik.uni-regensburg.de, tashi.walde@ma.tum.de Content-Type: multipart/alternative; boundary="000000000000e08e7505f5ef2aa0" 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=difu1QiU; spf=pass (google.com: domain of mathieu.anel@gmail.com designates 2a00:1450:4864:20::52c 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: , --000000000000e08e7505f5ef2aa0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable ~*~*~*~*~*~*~*~* CMU HoTT Seminar Online *~*~*~*~*~*~*~*~ The CMU team would like to invite all of you for a special series of 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 Monday March 13 (10am-12pm EST / 3pm-5pm CET / UTC-04:0= 0) Lecture 2 =E2=80=94 Monday March 20 (10am-12pm EST / 3pm-5pm CET / UTC-04:0= 0) Lecture 3 =E2=80=94 Monday March 27 (10am-12pm EST / 4pm-6pm CET / UTC-04:0= 0) (Beware that the time difference USA/Europe (EST/CET) is only 5h for the 13 & 20th and back to 6h for the 27th) 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 Meeting ID: 622 894 049 Passcode: the Brunerie number Our seminar page https://www.cmu.edu/dietrich/philosophy/hott/seminars/index.html --=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/CAD3N2UatUmLO8-evBsW-JyPVV6WG7S6yamzk5b_hYo9ArMv6eQ%40ma= il.gmail.com. --000000000000e08e7505f5ef2aa0 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

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


The CMU team would like to invite all of you for a special series of= lectures by


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

Hoang Kim Nguyen (Universit=C3=A4t Regensburg)<= /span>

Tashi Walde (Technische Universit=C3=A4t M=C3= =BCnchen)


<= p style=3D"color:rgb(0,0,0);font-size:14px;line-height:1.5;margin:0px;font-= family:system-ui,sans-serif">on=C2=A0** Univalent Directed Type Theory **

(abstract below)


Lecture 1 =E2=80=94 Monday March 13 (10= am-12pm EST / 3pm-5pm CET / UTC-04:00)

Lecture= 2 =E2=80=94 Monday March 20 (10am-12pm EST / 3pm-5pm CET / UTC-04:00)

Lecture 3 =E2=80=94 Monday March 27 (10am-12pm EST= / 4pm-6pm CET / UTC-04:00)


(Beware that the time difference USA/Eu= rope (EST/CET) is only 5h for the 13 & 20th and back to 6h for the 27th= )


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 fragment and an extension of or= dinary dependent type theory. The axioms are chosen so that (=E2=88=9E,1)= =E2=80=91category theory (under the form of quasi-categories or complete Se= gal spaces) gives a semantic interpretation, in a way which extends Voevods= ky's interpretation of univalent dependent type theory in the homotopy = theory of Kan complexes. More generally, using a slight generalization of S= hulman'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 dev= eloped by Martini and Wolf) is a semantic interpretation as well (hence so = is parametrized higher category theory introduced by Barwick, Dotto, Glasma= n, 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 sug= gested by the work of Licata and Weaver), or simplicial Hott (as in the wor= k of Buchholtz and Weinberger). We will explain the axioms in detail and ha= ve a glimpse at basic theorems and constructions in this context (Yoneda Le= mma, Kan extensions, Localizations). We will also discuss the perspective o= f reflexivity: since the theory speaks of itself (through directed univalen= ce), 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 rectifyi= ng 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 Mee= ting

https://cmu.zoom.us/j/622894049

Meeting ID: 622 894 = 049

Passcode: the Brunerie number



Our seminar page

https://www.cmu.edu/dietrich/philosophy/hott/s= eminars/index.html


--
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/CAD3N2UatUmLO8-evBsW-JyPVV6WG7S6y= amzk5b_hYo9ArMv6eQ%40mail.gmail.com.
--000000000000e08e7505f5ef2aa0--