Search

• < Previous
• 1
• Next >

---

LNL polycategories and doctrines of linear logic

Michael Shulman.

We define and study LNL polycategories, which abstract the judgmental structure of classical linear logic with exponentials. Many existing structures can be represented as LNL polycategories, including LNL adjunctions, linear exponential comonads, LNL multicategories, IL-indexed categories, linearly&nbsp;[&hellip;]

---

Modalities in homotopy type theory

Egbert Rijke ; Michael Shulman ; Bas Spitters.

Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and&nbsp;[&hellip;]

---

Idempotents in intensional type theory

Michael Shulman.

We study idempotents in intensional Martin-L\"of type theory, and in particular the question of when and whether they split. We show that in the presence of propositional truncation and Voevodsky's univalence axiom, there exist idempotents that do not split; thus in plain MLTT not all idempotents&nbsp;[&hellip;]

---