17 citations · 26 across the 5 of their papers we have counts for
5 papers · 1 filter
A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism
Marc Bezem, Thierry Coquand, Peter Dybjer +1
We present generalized algebraic theories corresponding to slightly modified versions of two of the type theories in our paper Type Theory with Explicit Universe Polymorphism. We f…
Type Theory with Explicit Universe Polymorphism (revised and extended version)
Marc Bezem, Thierry Coquand, Peter Dybjer +1
The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend on e…
Categories with Families: Unityped, Simply Typed, and Dependently Typed
Simon Castellan, Pierre Clairambault, Peter Dybjer
We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with family (cwf). To this end we i…
Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version)
Simon Castellan, Pierre Clairambault, Peter Dybjer
We show that a version of Martin-Löf type theory with an extensional identity type former I, a unit type N1 , Sigma-types, Pi-types, and a base type is a free category with familie…
The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
Pierre Clairambault, Peter Dybjer
Seely's paper "Locally cartesian closed categories and type theory" contains a well-known result in categorical type theory: that the category of locally cartesian closed categorie…