2 papers
cs.LO2026
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…
cs.LO2024
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…