Logo

Mathematical Sciences Research Institute

Home » HC Special Seminar - HoTT Electronic Seminar Talks (HoTTEST): The Constructive Kan-Quillen Model Structure

Seminar

HC Special Seminar - HoTT Electronic Seminar Talks (HoTTEST): The Constructive Kan-Quillen Model Structure February 20, 2020 (08:30 AM PST - 10:00 AM PST)
Parent Program:
Location: MSRI: Baker Board Room
Speaker(s) Karol Szumilo (Rheinische Friedrich-Wilhelms-Universit├Ąt Bonn)
Description No Description
Video
No Video Uploaded
Abstract/Media

The classical Kan--Quillen model structure on the category of simplicial sets is a fundamental object in homotopy theory. Many proofs of its existence have been found, but (until recently) all of them relied on principles of classical logic: the law of excluded middle and the axiom of choice. For the purposes of interpretation of Homotopy Type Theory, such arguments were insufficient.

A fully constructive proof is possible, but it requires a careful adjustment of the definitions of cofibrations and weak homotopy equivalences of simplicial sets. In the talk, I will outline one such constructive argument, explaining how various standard techniques of simplicial homotopy theory need to be adapted to constructive logic.

This is joint work with Nicola Gambino and Christian Sattler, inspired by Simon Henry who was the first to obtain the result.

No Notes/Supplements Uploaded No Video Files Uploaded