Search

• < Previous
• 1
• Next >

---

Constructing Higher Inductive Types as Groupoid Quotients

Niccolò Veltri ; Niels van der Weide.

In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. We define an internal notion of signatures for HITs, and for each signature, we construct a bicategory of&nbsp;[&hellip;]

---

Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory

Bassel Mannaa ; Rasmus Ejlers Møgelberg ; Niccolò Veltri.

Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning about advanced programming language features using an abstract form of step-indexing. CloTT has previously been shown to&nbsp;[&hellip;]

---