13 citations · 23 across the 7 of their papers we have counts for
9 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…
Bilimits in categories of partial maps
Jonathan Sterling
The closure of chains of embedding-projection pairs (ep-pairs) under bilimits in some categories of predomains and domains is standard and well-known. For instance, Scott's $D_\inf…
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…
Algebraic Type Theory and Universe Hierarchies
Jonathan Sterling
It is commonly believed that algebraic notions of type theory support only universes à la Tarski, and that universes à la Russell must be removed by elaboration. We clarify the sta…
Normalization by gluing for free λ-theories
Jonathan Sterling, Bas Spitters
The connection between normalization by evaluation, logical predicates and semantic gluing constructions is a matter of folklore, worked out in varying degrees within the literatur…