5 citations · 6 across the 2 of their papers we have counts for
5 papers · 1 filter
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…
An inductive-recursive universe generic for small families
Daniel Gratzer
We show that it is possible to construct a universe in all Grothendieck topoi with injective codes a la Pujet and Tabareau which is nonetheless generic for small families. As a tri…
Normalization for multimodal type theory
Daniel Gratzer
We consider the conversion problem for multimodal type theory (MTT) by characterizing the normal forms of the type theory and proving normalization. Normalization follows from a no…
Syntactic categories for dependent type theory: sketching and adequacy
Daniel Gratzer, Jonathan Sterling
We argue that locally Cartesian closed categories form a suitable doctrine for defining dependent type theories, including non-extensional ones. Using the theory of sketches, one m…
Cubical Syntax for Reflection-Free Extensional Equality
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
We contribute XTT, a cubical reconstruction of Observational Type Theory which extends Martin-Löf's intensional type theory with a dependent equality type that enjoys function exte…