*[HoTT] [CMU-HoTT] Special series of lectures — Cisinski, Nguyen, Walde on *Univalent Directed Type Theory*@ 2023-03-16 12:38 mathie...@gmail.com0 siblings, 0 replies; 3+ messages in thread From: mathie...@gmail.com @ 2023-03-16 12:38 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 3270 bytes --] ~*~*~*~*~*~*~*~* 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ät Regensburg) Hoang Kim Nguyen (Universität Regensburg) Tashi Walde (Technische Universität München) on *** Univalent Directed Type Theory *** (abstract below) Lecture 1 — video <https://www.youtube.com/watch?v=5YOltuTcBK8>, slides intro <https://www.cmu.edu/dietrich/philosophy/hott/seminars/slides/cisinski-nguyen-walde-intro_talk1.pdf> , slides talk <https://www.cmu.edu/dietrich/philosophy/hott/seminars/slides/cisinski-nguyen-walde-talk1.pdf> Next lectures Lecture 2 — *Monday March 20*(10am-12pm EDT / 3pm-5pm CET) Lecture 3 — 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‑categories. The axioms are both a fragment and an extension of ordinary dependent type theory. The axioms are chosen so that (∞,1)‑category 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 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 (∞,1)‑categories internally in any ∞‑topos (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 ∞‑cosmoi 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=bkhtRlNxL3E3SnZCTU1oSFNHcHJNQT09 Meeting ID: 622 894 049 Passcode: ‘the Brunerie number’ Seminar webpage https://www.cmu.edu/dietrich/philosophy/hott/seminars/index.html#230313 -- 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 email 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. [-- Attachment #1.2: Type: text/html, Size: 10684 bytes --] ^ permalink raw reply [flat|nested] 3+ messages in thread

*[HoTT] [CMU-HoTT] Special series of lectures — Cisinski, Nguyen, Walde on *Univalent Directed Type Theory*@ 2023-03-23 18:00 mathieu anel0 siblings, 0 replies; 3+ messages in thread From: mathieu anel @ 2023-03-23 18:00 UTC (permalink / raw) To: homotopytypetheory [-- Attachment #1: Type: text/plain, Size: 3181 bytes --] ~*~*~*~*~*~*~*~* CMU HoTT Seminar Online *~*~*~*~*~*~*~*~ Don't miss lecture 3 ! Denis-Charles Cisinski (Universität Regensburg) Hoang Kim Nguyen (Universität Regensburg) Tashi Walde (Technische Universität München) on *** Univalent Directed Type Theory *** (abstract below) Lecture 1 — video https://www.youtube.com/watch?v=5YOltuTcBK8 Slides intro https://www.cmu.edu/dietrich/philosophy/hott/seminars/slides/cisinski-nguyen-walde-intro_talk1.pdf Slides talk https://www.cmu.edu/dietrich/philosophy/hott/seminars/slides/cisinski-nguyen-walde-talk1.pdf Lecture 2 — video https://www.youtube.com/watch?v=xWmELBvHMPo Slides https://www.cmu.edu/dietrich/philosophy/hott/seminars/slides/cisinski-nguyen-walde-talk2.pdf *Next lecture* *Lecture 3 — 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‑categories. The axioms are both a fragment and an extension of ordinary dependent type theory. The axioms are chosen so that (∞,1)‑category 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 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 (∞,1)‑categories internally in any ∞‑topos (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 ∞‑cosmoi 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=bkhtRlNxL3E3SnZCTU1oSFNHcHJNQT09 Meeting ID: 622 894 049 Passcode: ‘the Brunerie number’ Seminar webpage https://www.cmu.edu/dietrich/philosophy/hott/seminars/index.html#230313 -- 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAD3N2UZznZkfh6rZTzg9YhP0gYiOfiq7gEVn78P-S99Yo1wXQw%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 10098 bytes --] ^ permalink raw reply [flat|nested] 3+ messages in thread

*[HoTT] [CMU-HoTT] Special series of lectures — Cisinski, Nguyen, Walde on *Univalent Directed Type Theory*@ 2023-03-11 22:15 mathieu anel0 siblings, 0 replies; 3+ messages in thread From: mathieu anel @ 2023-03-11 22:15 UTC (permalink / raw) To: homotopytypetheory [-- Attachment #1: Type: text/plain, Size: 3031 bytes --] ~*~*~*~*~*~*~*~* 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ät Regensburg) Hoang Kim Nguyen (Universität Regensburg) Tashi Walde (Technische Universität München) on *** Univalent Directed Type Theory *** (abstract below) Lecture 1 — Monday March 13 (10am-12pm EDT / 3pm-5pm CET / UTC-04:00) Lecture 2 — Monday March 20 (10am-12pm EDT / 3pm-5pm CET / UTC-04:00) Lecture 3 — 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‑categories. The axioms are both a fragment and an extension of ordinary dependent type theory. The axioms are chosen so that (∞,1)‑category 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 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 (∞,1)‑categories internally in any ∞‑topos (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 ∞‑cosmoi 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 -- 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAD3N2UZdVG39rA3UNTVeTr%3DRvsOm2RmbDUZpCd15c7T22ZhHPw%40mail.gmail.com. [-- Attachment #2: Type: text/html, Size: 8619 bytes --] ^ permalink raw reply [flat|nested] 3+ messages in thread

end of thread, other threads:[~2023-03-23 18:00 UTC | newest]Thread overview:3+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2023-03-16 12:38 [HoTT] [CMU-HoTT] Special series of lectures — Cisinski, Nguyen, Walde on *Univalent Directed Type Theory* mathie...@gmail.com -- strict thread matches above, loose matches on Subject: below -- 2023-03-23 18:00 mathieu anel 2023-03-11 22:15 mathieu anel

This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).