fun-with-cwf
Formalising iterative sets, and presheaves valued in them, as categories with families in Cubical Agda (work in progress)
with Anders Mörtberg & Élise Souche
About
An ongoing formalisation of categories with families (CwFs) and of the models of type theory built from iterative sets, written in Cubical Agda. The aim is to upstream the whole development into the cubical library.
Contents
- two presentations of a category with families — the algebraic one and the categorical one — together with translations in both directions
- the CwF of iterative sets, and the CwF of presheaves valued in iterative sets
- Π- and Σ-structures on these CwFs
- Tarski universes, with the iterative sets, the cumulative hierarchy, the finite sets and an inductive-recursive universe as instances
- a category whose finite-set-valued presheaves admit no Π-structure