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

---

Presentable signatures and initial semantics

Benedikt Ahrens ; André Hirschowitz ; Ambroise Lafont ; Marco Maggesi.

We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we study a notion of "signature" for specifying syntactic constructions. In the spirit of Initial Semantics, we define the "syntax generated by a signature" to be&nbsp;[&hellip;]

---