March 28: Evan Cavallo, Why some cubical models don't present spaces

[Dan Christensen]

This week the HoTTEST seminar presents:

Evan Cavallo

Why some cubical models don't present spaces

*Note that the seminar is on daylight time.*

The talk is at 11:30am *EDT* (15:30 UTC) on Thursday, March 28.
The talk will be 60 minutes long, followed by up to 30 minutes for
questions. See

https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html

for the Zoom link and a list of all upcoming talks.

All are welcome!

Abstract:

Historically, constructive cubical interpretations of HoTT interpret
types as families equipped with an "open box-filling" operation, which
ensures that identities in types can be interpreted as maps from an
interval. This choice of structure was inspired by Kan's early work on
cubical sets. However, cubical type theory inteprets in forms of cubical
sets not considered by Kan, indeed rarely considered in the
homotopy-theoretical literature. In these settings, it is a priori
unclear whether a box-filling operation is really what should qualify a
cubical set as a "space" in a standard sense. I'll present arguments
that for many forms of cubical set used in interpretations of HoTT, this
is in fact not the case. Concretely, we show that in these settings,
Quillen model structures based on box-filling fibrations are not Quillen
equivalent to model categories (such as the Kan-Quillen model structure
on simplicial sets) which do present spaces.

This is joint work with Christian Sattler.

Dan

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