February 20: Martín Escardó, Injective types

[Angiuli, Carlo]

This week in HoTTEST we are excited to host Martín Escardó, who will speak about "Injective types". (Abstract at the end of this email.) The talk is at 11:30am EST = 16:30 UTC this Thursday, February 20, and will be 60 minutes long followed by up to 30 minutes of discussion.

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

Further information, including videos and slides from past talks, is available at: https://www.math.uwo.ca/faculty/kapulkin/seminars/hottest.html

Carlo

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

--

Martín Hötzel Escardó

Injective types

In previous work, we established results about injective types in HoTT/UF, including characterizations, closure properties, and examples. In recent current work, in collaboration with Tom de Jong, we have developed more examples and counter-examples, as well as a better understanding of the landscape. In this talk I will present these old and new ideas.