Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: "mathie...@gmail.com" <mathieu.anel@gmail.com>
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: [HoTT] [CMU-HoTT] Special series of lectures — Cisinski, Nguyen, Walde on *Univalent Directed Type Theory*
Date: Thu, 16 Mar 2023 05:38:43 -0700 (PDT)	[thread overview]
Message-ID: <c864a21a-ba63-4e34-b174-e683d9afd132n@googlegroups.com> (raw)

[-- 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 
, slides talk 

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)


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’

Seminar webpage


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 --]

             reply	other threads:[~2023-03-16 12:38 UTC|newest]

Thread overview: 3+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2023-03-16 12:38 mathie...@gmail.com [this message]
  -- strict thread matches above, loose matches on Subject: below --
2023-03-23 18:00 mathieu anel
2023-03-11 22:15 mathieu anel

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=c864a21a-ba63-4e34-b174-e683d9afd132n@googlegroups.com \
    --to=mathieu.anel@gmail.com \
    --cc=HomotopyTypeTheory@googlegroups.com \


* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
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).