Search

• < Previous
• 1
• Next >

Categorical structures for type theory in univalent foundations

In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in univalent type theory, where the comparisons between them&nbsp;[&hellip;]