Loïc Pujet: Strictifying Categories with Families, part 2

Abstract

Last week, we saw how one can strictify the equations of a basic CwF in observational type theory by embedding it into its category of preasheaves. Unfortunately, this technique is not sufficient to handle CwFs with more structure (dependent products, inductive types, etc).

This week, I will explain how to use Pédrot's "prefascist sets" -- an alternative definition of presheaves that satisfy more definitional equations -- to obtain the remaining equations.

This is joint work with Ambrus Kaposi.