Search

• < Previous
• 1
• Next >

---

Multimodal Dependent Type Theory

Daniel Gratzer ; G. A. Kavvos ; Andreas Nuyts ; Lars Birkedal.

We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and&nbsp;[&hellip;]

---

Transpension: The Right Adjoint to the Pi-type

Andreas Nuyts ; Dominique Devriese.

Presheaf models of dependent type theory have been successfully applied to model HoTT, parametricity, and directed, guarded and nominal type theory. There has been considerable interest in internalizing aspects of these presheaf models, either to make the resulting language more expressive, or in&nbsp;[&hellip;]

---