4 papers
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.…
Higher Structures in Homotopy Type Theory
Ulrik Buchholtz
The intended model of the homotopy type theories used in Univalent Foundations is the infinity-category of homotopy types, also known as infinity-groupoids. The problem of higher s…
Higher Groups in Homotopy Type Theory
Ulrik Buchholtz, Floris van Doorn, Egbert Rijke
We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a point…
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…