The biequivalence of path categories and axiomatic Martin-Löf type theories

Daniël Otten, Matteo Spadetto

The semantics of extensional type theory has an elegant categorical description: models of extensional =-types, 1-types, and Sigma-types are biequivalent to finitely complete categ…