February 29: Rafaël Bocquet on "Strict Rezk completions of models of HoTT and homotopy canonicity".

[Emily Riehl]

In a special once every four years leap day edition, the HoTTEST seminar continues tomorrow, on Thursday, at the usual (winter) time, 11:30am EST = 16:30 UTC. 

Our speaker is Rafaël Bocquet, whose talk is titled "Strict Rezk completions of models of HoTT and homotopy canonicity".  The talk will be 60 minutes long, followed by
up to 30 minutes for questions.  The abstract is below.

The Zoom link is https://zoom.us/j/994874377

Further information, including the list of upcoming speakers, and videos and slides from past talks, is at:

https://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.uwo.ca%2Fmath%2Ffaculty%2Fkapulkin%2Fseminars%2Fhottest.html&data=05%7C02%7Ceriehl%40jhu.edu%7Cc97c6cad2d524bc89d3508dbfbd81a30%7C9fa4f438b1e6473b803f86f8aedf0dec%7C0%7C0%7C638380677789773347%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=YsbZeYYtwjLRvytq8cl27nopd66nONctu5pIO2MRjhM%3D&reserved=0

Emily

(On behalf of the HoTTEST organizers: Carlo Angiuli, Dan Christensen, Chris Kapulkin, and Emily Riehl.)

Title: Strict Rezk completions of models of HoTT and homotopy canonicity

Abstract:

 

In this talk I'll present the main ideas of my new proof of homotopy canonicity for HoTT (see arXiv:2311.05849).

Constructive models of HoTT, such as cubical set models, provide a computational interpretation of the univalence axiom. Homotopy
canonicity, originally conjectured by Voevodsky, implies that the computational content of univalence can already be observed in the
syntax.

Canonicity results are usually proven using a sconing construction, gluing together the syntax and a semantic model. For homotopy
canonicity, the semantic model should be a model of HoTT, say cubical sets. To carry out the sconing construction, the components of the
base model should also be cubical sets with the correct higher dimensional structure. However the components of the syntax are only
sets, which can be seen as discrete cubical sets, with the "wrong" higher dimensional structure.

This can be solved by constructing the "strict Rezk completion" of the syntax, which is an equivalent model with the correct higher
dimensional structure. Strict Rezk completions can be constructed in cartesian cubical sets.

 

-- 

Professor of Mathematics (she/her)
Johns Hopkins University
emilyriehl.github.io