Univalent Type Theorems: Models, Equalities, and Coherence

During the performance period of the grant, the PI, the PRDAs Karol Szumilo and Sina Hazratpour and the PIs PhD students developed research along three connected lines of enquiry: algebraic models of homotopy type theory, constructive models of univalent foundations, and connections between homotopy type theory and higher categories. Their research led to several key results, including a partial solution to the open problem of definining a constructive version of the simplicial model of univalent foundations. These results have already been used by researchers in the area and have been presented in several papers and preprints. The work has also opened up new research directions, such as a higher-categorical version of exact completions.