13 citations · 22 across the 7 of their papers we have counts for
10 papers
On symmetries of spheres in univalent foundations
Pierre Cagne, Ulrik Buchholtz, Nicolai Kraus +1
Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form . The case of the circle has a slick answer: th…
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…
A Note on Generalized Algebraic Theories and Categories with Families
Marc Bezem, Thierry Coquand, Peter Dybjer +1
We give a new syntax independent definition of the notion of a generalized algebraic theory as an initial object in a category of categories with families (cwfs) with extra structu…
Construction of the Circle in UniMath
Marc Bezem, Ulrik Buchholtz, Daniel R. Grayson +1
We show that the type of -torsors has the dependent universal property of the circle, which characterizes it up to a unique homotopy equivalence.…
Syntactic Forcing Models for Coherent Logic
Marc Bezem, Ulrik Buchholtz, Thierry Coquand
We present three syntactic forcing models for coherent logic. These are based on sites whose underlying category only depends on the signature of the coherent theory, and they do n…
The univalence axiom in cubical sets
Marc Bezem, Thierry Coquand, Simon Huber
In this note we show that Voevodsky's univalence axiom holds in the model of type theory based on symmetric cubical sets. We will also discuss Swan's construction of the identity t…