BEGIN:VCALENDAR
VERSION:2.0
METHOD:PUBLISH
CALSCALE:GREGORIAN
PRODID:-//WordPress - MECv5.22.3//EN
X-ORIGINAL-URL:https://eur.univ-paris13.fr/
BEGIN:VEVENT
UID:MEC-24e27b869b66e9e62724bd7725d5d9c1@eur.univ-paris13.fr
DTSTART:20260423T120000Z
DTEND:20260423T160000Z
DTSTAMP:20260421T131600Z
CREATED:20260421
LAST-MODIFIED:20260428
SUMMARY:Colloquium MathSTIC / EUR M&CS
DESCRIPTION:Le jeudi 23 avril 2026 à 14h\nLieu: Salle B405 du LAGA\nPossibilité de suivre en visio: https://bbb.math.univ-paris13.fr/b/chr-hyw-0rb-jz4\nLien de la rediffusion : https://bbb.math.univ-paris13.fr/playback/presentation/2.3/260aa433e092cf0e79b317a48abfe4178f8bd499-1776945086393\n\nTo watch the video in full screen, click on this icon : \n\nUlrik Buchholz\nUniversité de Nottingham\nhttps://ulrikbuchholtz.dk/\n \nThe infinity-category of infinity-categories in simplicial type theory\nIn univalent foundations, as proposed by Voevodsky, the basic objects are infinity-groupoids (or anima), so every construction and theorem respects the natural notion of equivalence for each type of mathematical object. A formal account of this is given by homotopy type theory (HoTT), based on Martin-Löf’s dependent type theory extended with Voevodsky’s univalence axiom. Univalent foundations should be an ideal setting for doing model-independent higher category theory. However, it’s still an open problem whether HoTT can define the infinity-groupoid of infinity-categories.\nRiehl and Shulman proposed an extension of HoTT, called simplicial type theory (STT), where the basic objects are simplicial infinity-groupoids. I will explain and motivate simplicial type theory, along with an extension that allows us to define the infinity-category of infinity-categories. The latter part is based on joint work with Daniel Gratzer and Jonathan Weinberger.\n \n
X-ALT-DESC;FMTTYPE=text/html:<p>Le jeudi 23 avril 2026 à 14h<br />
Lieu: Salle B405 du LAGA<br />
Possibilité de suivre en visio: <a class="moz-txt-link-freetext" href="https://bbb.math.univ-paris13.fr/b/chr-hyw-0rb-jz4">https://bbb.math.univ-paris13.fr/b/chr-hyw-0rb-jz4</a></p>
<p><strong>Lien de la rediffusion </strong>: h<a href="ttps://bbb.math.univ-paris13.fr/playback/presentation/2.3/260aa433e092cf0e79b317a48abfe4178f8bd499-1776945086393">ttps://bbb.math.univ-paris13.fr/playback/presentation/2.3/260aa433e092cf0e79b317a48abfe4178f8bd499-1776945086393</a></p>
<ul>
<li>To watch the video in full screen, click on this icon : <strong><img loading="lazy" src="https://eur.univ-paris13.fr/wp-content/uploads/2026/03/Capture-decran-2026-04-01-155206.png" alt="" width="32" height="29" /></strong></li>
</ul>
<p>Ulrik Buchholz<br />
Université de Nottingham<br />
<a class="moz-txt-link-freetext" href="https://ulrikbuchholtz.dk/">https://ulrikbuchholtz.dk/</a></p>
<p>&nbsp;</p>
<p><strong>The infinity-category of infinity-categories in simplicial type theory</strong></p>
<p>In univalent foundations, as proposed by Voevodsky, the basic objects are infinity-groupoids (or anima), so every construction and theorem respects the natural notion of equivalence for each type of mathematical object. A formal account of this is given by homotopy type theory (HoTT), based on Martin-Löf&#8217;s dependent type theory extended with Voevodsky&#8217;s univalence axiom. Univalent foundations should be an ideal setting for doing model-independent higher category theory. However, it&#8217;s still an open problem whether HoTT can define the infinity-groupoid of infinity-categories.</p>
<p>Riehl and Shulman proposed an extension of HoTT, called simplicial type theory (STT), where the basic objects are simplicial infinity-groupoids. I will explain and motivate simplicial type theory, along with an extension that allows us to define the infinity-category of infinity-categories. The latter part is based on joint work with Daniel Gratzer and Jonathan Weinberger.</p>
<p>&nbsp;</p>

URL:https://eur.univ-paris13.fr/events/colloquium-mathstic-eur-mcs/
ORGANIZER;CN=:MAILTO:
END:VEVENT
END:VCALENDAR