Search

• < Previous
• 1
• Next >

---

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

---

Displayed Categories

Benedikt Ahrens ; Peter LeFanu Lumsdaine.

We introduce and develop the notion of *displayed categories*. A displayed category over a category C is equivalent to "a category D and functor F : D --> C", but instead of having a single collection of "objects of D" with a map to the objects of C, the objects are given as a family indexed by&nbsp;[&hellip;]

---

Initial Semantics for Reduction Rules

Benedikt Ahrens.

We give an algebraic characterization of the syntax and operational semantics of a class of simply-typed languages, such as the language PCF: we characterize simply-typed syntax with variable binding and equipped with reduction rules via a universal property, namely as the initial object of some&nbsp;[&hellip;]

---