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 15480 invoked from network); 11 Mar 2023 22:16:11 -0000 Received: from mail-ed1-x53b.google.com (2a00:1450:4864:20::53b) by inbox.vuxu.org with ESMTPUTF8; 11 Mar 2023 22:16:11 -0000 Received: by mail-ed1-x53b.google.com with SMTP id y24-20020aa7ccd8000000b004be3955a42esf12160932edt.22 for ; Sat, 11 Mar 2023 14:16:11 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1678572971; cv=pass; d=google.com; s=arc-20160816; b=bhlRJIo3DlFIZQutWZmLebLx9d58zFXj5U8DZAtIXTq9EY/sN4143X7hrrbqHS4ynY zYbJRs+sA/nTvdaEg9PGqAGkubd6iloX7qDndb9G/fB8LDBwfL9wqGnx2e/Ip9/DEeCT CSXwd7jwVbW+kxcVcGIU9r2BEXpMxMbtYtJDE25BrCbPPQMKeK7Gedh9Yqc/A/3kQBS+ Elw8TU0YJRd5UvREzDBMbmaK+8PoQXjPYDv6GkZkL+7cLa2XnfQG7oGMhiy3QX9gZyT3 0PPYsdBTLA/dw+ju+njWGM9zclC+YsQsioxRJmuMr4e8OY8d7qH8j8HZ7guQt7+u9ISS hViQ== 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=mZ1D0u0rpKn+xYfy2rU1/OB/RezL0zjTAs4A7NeFOk0=; b=H9yscwndzn5n93djO1vLe2ZuCc0HHrJipcvOGy3PxSwzNTJl4talkMeJ4SvMf74NAK 0UZGU14YiOb7e6snfRSE8EMyPb6pcORByQryPoJ8oNPEBx+poHaGhViidaAxb+mR+idd nFMEWdelWviO8D2l2R0JXKFrFuGuf8Auy4tmOeDUYJSJU8/O3ebaZkWN/Og+ld5xswc3 Vj7oqz5HlbjLHBRJ8D2UaVcApKT9/C4yICaYjX2akn1IdIU8G8fw+SipwRlQDYskJddo b0Vtq7V6E7toxcvUTZ/EwobjQ/5BPYyh9ZJgTC99jEopNdxXovcur3wBDApGA874oHJS fY3g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=oE9KzpCs; spf=pass (google.com: domain of mathieu.anel@gmail.com designates 2a00:1450:4864:20::533 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=1678572971; 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=mZ1D0u0rpKn+xYfy2rU1/OB/RezL0zjTAs4A7NeFOk0=; b=hcqDO9arYSZ0DLDpzEfSGtA6IXcDBiIiqWbSIf2hOl37lRmVo84U2KblrBj7qUtAY8 uwCy1d5WwrVNZJ0Bgc0X/GgG5RK8aA+/terpy5KyyqlF/PdvqDDodaxiqUzkHcwIG/wa Rl37Vf2pdIBJq+ACTWjW0QuWvkdeRp1crSDBz3PErZY8RY6Z1j8oLhB3sqpgItuMlsFJ 93hbwJjWUM1KF0G9YK1EqE6x8Unlf+zGDCLlU2NHxKSQ8hpkFZO5df5rrzb488IxlEJy QefmiU8ioFxgQkSM80L2BWv9oDvBL/S20umLzZQFb/nHkg2xMnSrl3oDYv/Z5sPNviH3 XP2A== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; t=1678572971; 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=mZ1D0u0rpKn+xYfy2rU1/OB/RezL0zjTAs4A7NeFOk0=; b=oAOYxFgjLWP1FxXi7dllkzL3puPWgf38+dnIvRYroNvVcBiUiVDuuZLWZPWpOLe0ef LSCyPdYd0ofmT894K3mgUzp1aQgIh55eqvSVxiZJjj7kd8eS0KJ3EUEHOm2IrKbEJqsf Z74WU50w1T757baFBXVqaeXwaTn4fjIfj0vwS5aeKX1J7z+yl/WAk464onkFoU+G714v KbttqViAn9HywWyEHGBaKUtyv2NyZ8irrZWGMAJAWoRaLd7pzkbaV08m+FkjsTfsJJyU +gSJ3EwXuT9IxD8NNtHDgk098bWo5Vds1w4ZFrJSqEgOqoSXVi0pr92tO41VfS43XRhB q7CQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; t=1678572971; 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=mZ1D0u0rpKn+xYfy2rU1/OB/RezL0zjTAs4A7NeFOk0=; b=iR6fk9Z5fFF1lrgupQQ0OXLfVDiKkz3rwfMeqIK2fvIwkazTrXo70LUlaxRcM/rRNF bI9KyFjL40p7DislbNxBG2f0UqTW88p3x/LJyAv/1MB1VEXWltOzOEx9WVwJVFyzIHN+ A/n8En9+Zib/XendbHS1M/FK6pyLt958XonuhXI2MjeCX/pb7IA7TvuzE+F2cyTeCF3m MTFwMwIvkYRU8+xkN8OtIo6MDC5t0/TByAk9dx0n5Atq0Cy+oJBMvrLc++dDxBte3hXv pYk8hbyTasoJ1TWkBpORGgpErcG8lUf+pxbl2mi8UrGVb8PPaAnNGa/2exFnV6Me98yy Vacg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AO0yUKWnAWKxGWVUY+Qq+7RWwFDcL7dhOKMl0JFpdEIj1I+XOcs7E49i ITo8+MwX/cX5/QBdxWSjSuk= X-Google-Smtp-Source: AK7set/N1F9Efus8A8jIPDqnoLcoKxCwH2fH+7jrNzqIjAEIIr4w3zTaCA/bT8BtN0MY908C1lDRew== X-Received: by 2002:a50:ce1c:0:b0:4fb:2593:846 with SMTP id y28-20020a50ce1c000000b004fb25930846mr640712edi.3.1678572970563; Sat, 11 Mar 2023 14:16:10 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:e081:b0:8b1:3554:9966 with SMTP id gh1-20020a170906e08100b008b135549966ls5587852ejb.2.-pod-prod-gmail; Sat, 11 Mar 2023 14:16:07 -0800 (PST) X-Received: by 2002:a17:906:fe09:b0:8b1:2bde:5c70 with SMTP id wy9-20020a170906fe0900b008b12bde5c70mr39467932ejb.2.1678572967760; Sat, 11 Mar 2023 14:16:07 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1678572967; cv=none; d=google.com; s=arc-20160816; b=xivijKyH6iMOufYG5RbBEpyyFSk0EEHqK5AhsOUcs8Kq2Y8fgIuhm1ifzj2M7EebKC 0ReOEMmVgBCvGuMyFB8Q7xu07V8linHGxrZeDGOKyPpv/y3XPJhzRwXf3LNYKPPnsuZi Jw/6pUtCABq33CH27+kVNh5r1Aofvwo92UOqtMckV4+cHovW6x/b1jL1IRHPZs6JGNaH ueI5s+ZafwPcaPUKqFH+d0Zv8v/Q2qkkeBMNARx89LjxgSCiwRHcAIs0905J26l9LNSW fgJJBxirr4Yn3B9hV5UCToqTNPEh0eAiKMTXiwtbtGWq3cZxpb05B1YZwYvUPrUEsbqZ tkzw== 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=tCq94R6zdhViRMXyhQswx1Q33v/tNaT5SXcNW2+0LgY=; b=QHmQkdCR1dMxUA/F56IvSAoVWKNsMKNQsj3j9mjTRvgXWVYMDt5xM4lHZOHcOrRkyj kYpyhlS0RvBq/YG5UW1czvBENytgg9sXzQPjqUNLe88PFsMt38aUMQFeV6fdZcTakKD6 jfW7p30AZHt/DcmtVyysX0dKNOKuFNfZg5/IuPZxF0nocKNl8REY826/Pqv7qa34qL0s 9WNA1r4Ak0OLokW0i9YDtnXxDSzvk43xLu2FXMgo2sDHqwpmeZOM2HjM7LkNGMe80xjj 6MTrlNpt0B9aSDLvdkz887AqTSyUMuOnV0wvDqL79nSi+U7QRQ3yP/ysST2V1cgzGzXJ 8Z0Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=oE9KzpCs; spf=pass (google.com: domain of mathieu.anel@gmail.com designates 2a00:1450:4864:20::533 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-x533.google.com (mail-ed1-x533.google.com. [2a00:1450:4864:20::533]) by gmr-mx.google.com with ESMTPS id kt6-20020a170906aac600b008dbae985b18si237178ejb.0.2023.03.11.14.16.07 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 11 Mar 2023 14:16:07 -0800 (PST) Received-SPF: pass (google.com: domain of mathieu.anel@gmail.com designates 2a00:1450:4864:20::533 as permitted sender) client-ip=2a00:1450:4864:20::533; Received: by mail-ed1-x533.google.com with SMTP id y4so5115456edo.2 for ; Sat, 11 Mar 2023 14:16:07 -0800 (PST) X-Received: by 2002:a17:906:80c1:b0:8b2:94c1:9e8f with SMTP id a1-20020a17090680c100b008b294c19e8fmr15622750ejx.12.1678572967360; Sat, 11 Mar 2023 14:16:07 -0800 (PST) MIME-Version: 1.0 From: mathieu anel Date: Sat, 11 Mar 2023 17:15:56 -0500 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="00000000000072fee605f6a7391d" 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=oE9KzpCs; spf=pass (google.com: domain of mathieu.anel@gmail.com designates 2a00:1450:4864:20::533 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: , --00000000000072fee605f6a7391d 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 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 EDT / 3pm-5pm CET / UTC-04:0= 0) Lecture 2 =E2=80=94 Monday March 20 (10am-12pm EDT / 3pm-5pm CET / UTC-04:0= 0) Lecture 3 =E2=80=94 Monday March 27 (10am-12pm EDT / 4pm-6pm CEST / UTC-04:= 00) Beware the time difference USA/Europe (EDT/CET) is only 5h for the 13 & 20th but 6h for the 27th (EDT/CEST). *The lectures will be recorded.* 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 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/CAD3N2UZdVG39rA3UNTVeTr%3DRvsOm2RmbDUZpCd15c7T22ZhHPw%40= mail.gmail.com. --00000000000072fee605f6a7391d Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

~*~*~*~*~*~*~*~* CM= U 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 (U= niversit=C3=A4t Regensburg)

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

on=C2=A0** Unival= ent Directed Type Theory **=C2=A0

(abstract b= elow)


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

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

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


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


= The lectures will be recorded.



Abstract:


= We will introduce a version of dependent type theory that is suitable to de= velop a synthetic theory of 1=E2=80=91categories. The axioms are both a fra= gment and an extension of ordinary dependent type theory. The axioms are ch= osen so that (=E2=88=9E,1)=E2=80=91category theory (under the form of quasi= -categories or complete Segal spaces) gives a semantic interpretation, in a= way which extends Voevodsky's interpretation of univalent dependent ty= pe theory in the homotopy theory of Kan complexes. More generally, using a = slight generalization of Shulman's methods, we should be able to see th= at 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 interpre= tation as well (hence so is parametrized higher category theory introduced = by Barwick, Dotto, Glasman, Nardin and Shah). There are of course strong li= nks with =E2=88=9E=E2=80=91cosmoi of Riehl and Verity as well as with cubic= al Hott (as strongly suggested by the work of Licata and Weaver), or simpli= cial 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 d= iscuss the perspective of reflexivity: since the theory speaks of itself (t= hrough directed univalence), we can use it to justify new deduction rules t= hat express the idea of working up to equivalence natively (e.g. we can pro= duce a logic by rectifying the idea of having a locally cartesian type). In= particular, this logic can be used to produce and study semantic interpret= ations of Hott.



Link= for the Zoom Meeting

https://cmu.zoom.us/j/6= 22894049

Meeting ID: 622 894 049

Passcode: the Brunerie number


Semina= r webpage

https://www.cmu.edu/dietrich/philosophy/hott/seminars/inde= x.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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAD3N2UZdVG39rA3UNTVeTr%3DRvsOm= 2RmbDUZpCd15c7T22ZhHPw%40mail.gmail.com.
--00000000000072fee605f6a7391d--