November 6: Stefania Damato on "The Groupoid CwF of Containers"

[Angiuli, Carlo]

The HoTTEST seminar continues this Thursday, November 6 at 11:30 AM EST (UTC-5) / 16:30 UTC. Note that the US and Canada have just switched to winter time, although most of you will continue to experience HoTTEST at the usual local time. This week we present:

Stefania Damato

The Groupoid CwF of Containers

Abstract: The original definition of a category with families (CwF) gives rise to some coherence issues when working intensionally. For example, the set model and the presheaf model technically do not fit this definition because their collections of types form groupoids and not h-sets. Altenkirch and Kaposi have previously introduced a CwF of containers which suffers from similar coherence issues in the intensional setting. In this talk, I will present ongoing work on fixing these issues for the container case by defining a groupoid CwF (GCwF) of containers. A GCwF allows us to have types forming groupoids, while requiring us to prove some extra coherences.

As usual, the talk will be on Zoom: https://zoom.us/j/994874377

and you can find more information about HoTTEST, including past talks, at our new website: https://hottest-seminar.github.io/

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