Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] Special series of lectures — Cisinski, Nguyen, Walde on *Univalent Directed Type Theory*
@ 2023-03-02 18:40 mathieu anel
  0 siblings, 0 replies; only message in thread
From: mathieu anel @ 2023-03-02 18:40 UTC (permalink / raw)
  To: homotopytypetheory, cmu-hott
  Cc: Denis-Charles Cisinski, hoang-kim.nguyen, tashi.walde

[-- Attachment #1: Type: text/plain, Size: 2979 bytes --]

~*~*~*~*~*~*~*~* 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ä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 EST / 3pm-5pm CET / UTC-04:00)

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

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

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


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

Link for the Zoom Meeting


Meeting ID: 622 894 049

Passcode: the Brunerie number

Our seminar page


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/CAD3N2UatUmLO8-evBsW-JyPVV6WG7S6yamzk5b_hYo9ArMv6eQ%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 8288 bytes --]

^ permalink raw reply	[flat|nested] only message in thread

only message in thread, other threads:[~2023-03-02 18:40 UTC | newest]

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-03-02 18:40 [HoTT] Special series of lectures — Cisinski, Nguyen, Walde on *Univalent Directed Type Theory* 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).