36 citations · 143 across the 40 of their papers we have counts for
12 papers · 1 filter
Constructive theory of ordinals
Thierry Coquand, Henri Lombardi, Stefan Neuwirth
In Chapter 3 of his Notes on constructive mathematics, Martin-L{ö}f describes recursively constructed ordinals. He gives a constructively acceptable version of Kleene's computable…
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…
Canonicity and homotopy canonicity for cubical type theory
Thierry Coquand, Simon Huber, Christian Sattler
Cubical type theory provides a constructive justification of homotopy type theory. A crucial ingredient of cubical type theory is a path lifting operation which is explained comput…
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…
An introduction to Lorenzen's "Algebraic and logistic investigations on free lattices" (1951)
Thierry Coquand, Henri Lombardi, Stefan Neuwirth
Lorenzen's ``Algebraische und logistische Untersuchungen über freie Verbände'' appeared in 1951 in The Journal of Symbolic Logic. These ``Investigations'' have immediately been rec…
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…
Lattice-ordered groups generated by an ordered group and regular systems of ideals
Thierry Coquand, Henri Lombardi, Stefan Neuwirth
Unbounded entailment relations, introduced by Paul Lorenzen (1951), are a slight variant of a notion which plays a fundamental rôle in logic (see Scott 1974) and in algebra (see Lo…
A Sheaf Model of the Algebraic Closure
Bassel Mannaa, Thierry Coquand
In constructive algebra one cannot in general decide the irreducibility of a polynomial over a field K. This poses some problems to showing the existence of the algebraic closure o…
Constructive Theory of Banach algebras
Thierry Coquand, Bas Spitters
We present a way to organize a constructive development of the theory of Banach algebras, inspired by works of Cohen, de Bruijn and Bishop. We illustrate this by giving elementary…
Metric complements of overt closed sets
Thierry Coquand, Erik Palmgren, Bas Spitters
We show that the set of points of an overt closed subspace of a metric completion of a Bishop-locally compact metric space is located. Consequently, if the subspace is, moreover, c…
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…