Internal constructions in homotopical type theory
Publication Date
December 31, 2025
Creator
Abstract
The aim of this thesis is to investigate certain constructions that resist satisfactory full internalizations in plain homotopy type theory, i.e. intensional Martin-Löf type theory with the univalence axiom.
In Part I, we study internal higher categorical models of homotopical type theory, via wild categories with families (cwfs). We formulate coherence conditions on wild cwfs that suffice to recover properties expected of models of dependent type theory. The result is a definition of a 2-coherent wild cwf, which admits as instances both the syntax and the "standard model" given by a universe type. We also identify a higher "splitness" coherence condition that is satisfied by all set-level cwfs and univalent 2-coherent wild cwfs.
In Part II, we apply some of the theory developed in Part I and report on a partial investigation into the construction of type-valued Reedy-fibrant inverse diagrams in plain HoTT.
Item Type
ethesis
Thesis Type
PhD
Supervisors
Subjects (LC)
Associated Schools / Departments
School of Computer Science (UK)
eprints ID
81663
UoN Repository URI
Except where otherwise noted, this item's license is described as
File(s)![Thumbnail Image]()
Name
thesis.pdf
Type
Full-text
Description
Examined. Final version with corrections
Size
738.26 KB
Format
Adobe PDF
Checksum (MD5)
059e2f248539c8bd9412f1d13ba164e8