28 citations · 116 across the 28 of their papers we have counts for
10 papers · 1 filter
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…
Reflections on existential types
Jonathan Sterling
Existential types are reconstructed in terms of small reflective subuniverses and dependent sums. The folklore decomposition detailed here gives rise to a particularly simple accou…
Controlling unfolding in type theory
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli +2
We present a new way to control the unfolding of definitions in dependent type theory. Traditionally, proof assistants require users to fix whether each definition will or will not…
Classifying topoi in synthetic guarded domain theory
Daniele Palombi, Jonathan Sterling
Several different topoi have played an important role in the development and applications of synthetic guarded domain theory (SGDT), a new kind of synthetic domain theory that abst…
What should a generic object be?
Jonathan Sterling
Jacobs has proposed definitions for (weak, strong, split) generic objects for a fibered category; building on his definition of (split) generic objects, Jacobs develops a menagerie…
Denotational semantics of general store and polymorphism
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
We contribute the first denotational semantics of polymorphic dependent type theory extended by an equational theory for general (higher-order) reference types and recursive types,…