74 citations · 888 across the 55 of their papers we have counts for
62 papers
Doubly weak double categories
Aaron David Fairbanks, Michael Shulman
We propose a definition of double categories whose composition of 1-cells is weak in both directions. Namely, a doubly weak double category is a double computad -- a structure with…
Displayed Type Theory and Semi-Simplicial Types
Astra Kolomatskaia, Michael Shulman
We introduce Displayed Type Theory (dTT), a multi-modal homotopy type theory with discrete and simplicial modes. In the intended semantics, the discrete mode is interpreted by a mo…
Internal parametricity, without an interval
Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi +1
Parametricity is a property of the syntax of type theory implying, e.g., that there is only one function having the type of the polymorphic identity function. Parametricity is usua…
Semantics of multimodal adjoint type theory
Michael Shulman
We show that contrary to appearances, Multimodal Type Theory (MTT) over a 2-category M can be interpreted in any M-shaped diagram of categories having, and functors preserving, M-s…
On the -topos semantics of homotopy type theory
Emily Riehl
Many introductions to homotopy type theory and the univalence axiom gloss over the semantics of this new formal system in traditional set-based foundations. This expository article…
The directed plump ordering
Daniel Gratzer, Michael Shulman, Jonathan Sterling
Based on Taylor's hereditarily directed plump ordinals, we define the directed plump ordering on W-types in Martin-Löf type theory. This ordering is similar to the plump ordering b…