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-49d4b2faeb4b7b9e745775793141e2b2@eur.univ-paris13.fr
DTSTART:20260423T120000Z
DTEND:20260423T160000Z
DTSTAMP:20260421T131600Z
CREATED:20260421
LAST-MODIFIED:20260428
SUMMARY:Colloquium MathSTIC / EUR M&CS
DESCRIPTION:Thursday 23 April 2026 at 2.00 pm\nVenue: Room B405, LAGA\nAvailable to watch online: https://bbb.math.univ-paris13.fr/b/chr-hyw-0rb-jz4\nLink to the replay : 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\nUniversity of 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>Thursday 23 April 2026 at 2.00 pm<br />
Venue: Room B405, LAGA<br />
Available to watch online: https://bbb.math.univ-paris13.fr/b/chr-hyw-0rb-jz4</p>
<p><strong>Link to the replay </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 />
University of 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/en/events/colloquium-mathstic-eur-mcs-2/
ORGANIZER;CN=:MAILTO:
END:VEVENT
END:VCALENDAR