36 citations · 55 across the 9 of their papers we have counts for
5 papers · 1 filter
Constructive sheaf models of type theory
Thierry Coquand, Fabian Ruch, Christian Sattler
We generalise sheaf models of intuitionistic logic to univalent type theory over a small category with a Grothendieck topology. We use in a crucial way that we have constructive mo…
Regular entailment relations
Thierry Coquand, Henri Lombardi, Stefan Neuwirth
Inspired by the work of Lorenzen on the theory of preordered groups in the forties and fifties, we define regular entailment relations and show a crucial theorem for this structure…
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…
Integrals and Valuations
Thierry Coquand, Bas Spitters
We construct a homeomorphism between the compact regular locale of integrals on a Riesz space and the locale of (valuations) on its spectrum. In fact, we construct two geometric th…