Search

• < Previous
• 1
• Next >

---

Weak omega-categories from intensional type theory

Peter LeFanu Lumsdaine.

We show that for any type in Martin-L\"of Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. Precisely, we construct a contractible globular operad of definable composition laws, and give an action of this operad on the&nbsp;[&hellip;]

---

Categorical structures for type theory in univalent foundations

Benedikt Ahrens ; Peter LeFanu Lumsdaine ; Vladimir Voevodsky.

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;]

---