Loïc Pujet: Pre-fascism and the thin blue cubes

Abstract

Presheaves are a fundamental construction in category theory, and the basis of the cubical models of univalence. But interestingly enough, presheaves do not play so well with homotopy type theory: because of the higher dimensional structure of types, a correct definition of a Type-valued functor requires infinitely many coherence equations.

In his paper [Russian Constructivism in a Prefascist Theory], Pédrot introduces the "prefascist sets", a strictified presentation of presheaves: they satisfy the functoriality equations definitionally, and thus they automatically have all the higher coherence laws. Pédrot then uses prefascist sets to give a presheaf model of type theory internally to type theory.

In this talk, we will dissect Pédrot's construction, build higher dimensional variations, and use fibrant prefascist sets to give an internal model of univalence in observational type theory.