SU\G(𝔸)/K·U
Sign Up for free Log In

Author Description

Login to generate an author description

Ask a Question About This Mathematician

All published works (154)

A foundation for synthetic algebraic geometry

2024-12-04
Felix Cherubini , Thierry Coquand , Matthias Hutzler
Abstract This is a foundation for algebraic geometry, developed internal to the Zariski topos, building on the work of Kock and Blechschmidt (Kock (2006) [I.12], Blechschmidt (2017)). The Zariski topos … Abstract This is a foundation for algebraic geometry, developed internal to the Zariski topos, building on the work of Kock and Blechschmidt (Kock (2006) [I.12], Blechschmidt (2017)). The Zariski topos consists of sheaves on the site opposite to the category of finitely presented algebras over a fixed ring, with the Zariski topology, that is, generating covers are given by localization maps for finitely many elements $f_1,\dots, f_n$ that generate the ideal $(1)=A\subseteq A$ . We use homotopy-type theory together with three axioms as the internal language of a (higher) Zariski topos. One of our main contributions is the use of higher types – in the homotopical sense – to define and reason about cohomology. Actually computing cohomology groups seems to need a principle along the lines of our “Zariski local choice” axiom, which we justify as well as the other axioms using a cubical model of homotopy-type theory.
Chat View PDF

A Foundation for Synthetic Stone Duality

2024-12-04
Felix Cherubini , Thierry Coquand , Freek Geerligs +1 more
The language of homotopy type theory has proved to be appropriate as an internal language for various higher toposes, for example with Synthetic Algebraic Geometry for the Zariski topos. In … The language of homotopy type theory has proved to be appropriate as an internal language for various higher toposes, for example with Synthetic Algebraic Geometry for the Zariski topos. In this paper we apply such techniques to the higher topos corresponding to the light condensed sets of Dustin Clausen and Peter Scholze. This seems to be an appropriate setting to develop synthetic topology, similar to the work of Mart\'in Escard\'o. To reason internally about light condensed sets, we use homotopy type theory extended with 4 axioms. Our axioms are strong enough to prove Markov's principle, LLPO and the negation of WLPO. We also define a type of open propositions, inducing a topology on any type. This leads to a synthetic topological study of (second countable) Stone and compact Hausdorff spaces. Indeed all functions are continuous in the sense that they respect this induced topology, and this topology is as expected for these classes of types. For example, any map from the unit interval to itself is continuous in the usual epsilon-delta sense. We also use the synthetic homotopy theory given by the higher types of homotopy type theory to define and work with cohomology. As an application, we prove Brouwer's fixed-point theorem internally.
Chat View PDF

The equivariant model structure on cartesian cubical sets

2024-06-26
Steve Awodey , Evan Cavallo , Thierry Coquand +2 more
We develop a constructive model of homotopy type theory in a Quillen model category that classically presents the usual homotopy theory of spaces. Our model is based on presheaves over … We develop a constructive model of homotopy type theory in a Quillen model category that classically presents the usual homotopy theory of spaces. Our model is based on presheaves over the cartesian cube category, a well-behaved Eilenberg-Zilber category. The key innovation is an additional equivariance condition in the specification of the cubical Kan fibrations, which can be described as the pullback of an interval-based class of uniform fibrations in the category of symmetric sequences of cubical sets. The main technical results in the development of our model have been formalized in a computer proof assistant.
Chat View PDF

Projective Space in Synthetic Algebraic Geometry

2024-05-22
Felix Cherubini , Thierry Coquand , Matthias Hutzler +1 more
Working in an abstract, homotopy type theory based axiomatization of the higher Zariski-topos called synthetic algebraic geometry, we show that the Picard group of projective n-space is the integers, the … Working in an abstract, homotopy type theory based axiomatization of the higher Zariski-topos called synthetic algebraic geometry, we show that the Picard group of projective n-space is the integers, the automorphism group of projective n-space is PGL(n+1) and morphisms between projective standard spaces are given by homogenous polynomials in the usual way.
Chat View PDF

The Regular Element Property in Constructive Mathematics

2024-01-28
Thierry Coquand
The goal of this note is to present Kaplansky's proof of the Regular Element Property and to explain how this argument can be adapted to the case of a coherent, … The goal of this note is to present Kaplansky's proof of the Regular Element Property and to explain how this argument can be adapted to the case of a coherent, strongly discrete and Noetherian (with an inductive definition of Noetherian) rings in a constructive setting. We thus get, in this setting, an algorithm which given a f.g. regular ideal, build a regular element in this ideal.
Chat View PDF

In 1955, Paul Lorenzen clears the sky in foundations of mathematics for Hermann Weyl

2024-01-01
Stefan Neuwirth , Henri Lombardi , Thierry Coquand
In 1955, Paul Lorenzen is a mathematician who devotes all his research to foundations of mathematics, on a par with Hans Hermes, but his academic background is algebra in the … In 1955, Paul Lorenzen is a mathematician who devotes all his research to foundations of mathematics, on a par with Hans Hermes, but his academic background is algebra in the tradition of Helmut Hasse and Wolfgang Krull. This shift from algebra to logic goes along with his discovery that his ``algebraic works [...] have been concerned with a problem that has formally the same structure as the problem of consistency of the classical calculus of logic'' (letter to Carl Friedrich Gethmann dated 14 January 1988). After having provided a proof of consistency for arithmetic in 1944 and published it in 1951, Lorenzen inquires still further into the foundations of mathematics and arrives at the conviction that analysis can also be given a predicative foundation. Wilhelm Ackermann as well as Paul Bernays have pointed out to him in 1947 that his views are very close to those proposed by Hermann Weyl in Das Kontinuum (1918): sets are not postulated to exist beforehand; they are being generated in an ongoing process of comprehension. This seems to be the reason for Lorenzen to get into contact with Weyl, who develops a genuine interest into Lorenzen's operative mathematics and welcomes with great enthusiasm his Einf{\"u}hrung in die operative Logik und Mathematik (1955), which he studies line by line. This book's aim is to grasp the objects of analysis by means of inductive definitions; the most famous achievement of this enterprise is a generalised inductive formulation of the Cantor-Bendixson theorem that makes it constructive. This mathematical kinship is brutally interrupted by Weyl's death in 1955; a planned visit by Lorenzen at the Institute for Advanced Study in Princeton takes place only in 1957--1958. As told by Kuno Lorenz, Lorenzen's first Ph.D. student, a discussion with Alfred Tarski during this visit provokes a turmoil in Lorenzen's operative research program that leads to his abandonment of language levels and to a great simplification of his presentation of analysis by distinguishing only between ``definite'' and ``indefinite'' quantifiers: the former govern domains for which a proof of consistency is available and secures the use of the law of excluded middle; the latter govern those for which there isn't, e.g. the real numbers. Lorenzen states in his foreword to Differential und Integral (1965) that he is faithful to Weyl's approach of Das Kontinuum in this simplification. This history motivates a number of mathematical and philosophical issues about predicative mathematics: how does Weyl's interest into Lorenzen's operative mathematics fit with his turn to Brouwer's intuitionism as expressed in ``{\"U}ber die neue Grundlagenkrise der Mathematik'' (1921)? Why does Lorenzen turn away from his language levels and how does this turn relate to Weyl's conception of predicative mathematics? What do Lorenzen's conceptions of mathematics reveal about Weyl's conceptions?
Chat View PDF

Some Remarks About Dependent Type Theory

2023-10-11
Thierry Coquand

Reduction Free Normalisation for a proof irrelevant type of propositions

2023-07-13
Thierry Coquand
We show normalisation and decidability of convertibility for a type theory with a hierarchy of universes and a proof irrelevant type of propositions, close to the type system used in … We show normalisation and decidability of convertibility for a type theory with a hierarchy of universes and a proof irrelevant type of propositions, close to the type system used in the proof assistant Lean. Contrary to previous arguments, the proof does not require explicitly to introduce a notion of neutral and normal forms.
Chat View PDF

Constructive Theory of Ordinals

2023-04-01
Thierry Coquand , Henri Lombardi , Stefan Neuwirth
Martin-Löf [1970] describes recursively constructed ordinals.He gives a constructively acceptable version of Kleene's computable ordinals.In fact, the Turing definition of computable functions is not needed from a constructive point of … Martin-Löf [1970] describes recursively constructed ordinals.He gives a constructively acceptable version of Kleene's computable ordinals.In fact, the Turing definition of computable functions is not needed from a constructive point of view.We give in this paper a constructive theory of ordinals that is similar to Martin-Löf's theory, but based only on the two relations "x y" and "x < y", i.e. without considering sequents whose intuitive meaning is a classical disjunction.In our setting, the operation "supremum of ordinals" plays an important rôle through its interactions with the relations "x y" and "x < y".This allows us to approach as much as we may the notion of linear order when the property "α β or β α" is provable only within classical logic.Our aim is to give a formal definition corresponding to intuition, and to prove that our constructive ordinals satisfy constructively all desirable properties.
Chat View PDF

Constructive Remarks on Azumaya Algebra

2023-01-01
Thierry Coquand , Henri Lombardi , Stefan Neuwirth
We study etale topology and the notion of Azumaya algebra over a commutative ring constructively. As an application of the syntactic version of Barr's Theorem, we show the equivalence between … We study etale topology and the notion of Azumaya algebra over a commutative ring constructively. As an application of the syntactic version of Barr's Theorem, we show the equivalence between two definitions of Azumaya algebra.
Chat View PDF

A Foundation for Synthetic Algebraic Geometry

2023-01-01
Felix Cherubini , Thierry Coquand , Matthias Hutzler
This is a foundation for algebraic geometry, developed internal to the Zariski topos, building on the work of Kock and Blechschmidt. The Zariski topos consists of sheaves on the site … This is a foundation for algebraic geometry, developed internal to the Zariski topos, building on the work of Kock and Blechschmidt. The Zariski topos consists of sheaves on the site opposite to the category of finitely presented algebras over a fixed ring, with the Zariski topology, i.e. generating covers are given by localization maps $A\to A_{f_1}$ for finitely many elements $f_1,\dots,f_n$ that generate the ideal $(1)=A\subseteq A$. We use homotopy type theory together with three axioms as the internal language of a (higher) Zariski topos. One of our main contributions is the use of higher types -- in the homotopical sense -- to define and reason about cohomology. Actually computing cohomology groups, seems to need a principle along the lines of our ``Zariski local choice'' axiom, which we justify as well as the other axioms using a cubical model of homotopy type theory.
Chat View PDF

A variation of Reynolds-Hurkens Paradox

2023-01-01
Thierry Coquand
We present a variation of Hurkens paradox, which can itself be seen as a variation of Reynolds result that there is no set theoretic model of polymorphism. We present a variation of Hurkens paradox, which can itself be seen as a variation of Reynolds result that there is no set theoretic model of polymorphism.
Chat View PDF

Heitman dimension of distributive lattices and commutative rings

2023-01-01
Thierry Coquand , Henri Lombardi , Claude Quitté
This paper is the English translation of the first 4 sections of the article "Thierry Coquand, Henri Lombardi, and Claude Quitt\'e. Dimension de Heitmann des treillis distributifs et des anneaux … This paper is the English translation of the first 4 sections of the article "Thierry Coquand, Henri Lombardi, and Claude Quitt\'e. Dimension de Heitmann des treillis distributifs et des anneaux commutatifs. Publications Math\'ematiques de l'Universit\'e de Franche-Comt\'e, Besan\c{c}on. Alg\`ebre et th\'eorie des nombres. (2006)", after some corrections. Sections 5-7 of the original article are treated a bit more simply in the book "Henri Lombardi and Claude Quitt\'e. Commutative algebra: constructive methods. Finite projective modules. Algebra and applications, 20, Springer, Dordrecht, 2015." We study the notion of dimension introduced by Heitmann in his remarkable article "Raymond Heitmann. Generating non-Noetherian modules efficiently, Mich. Math. J., 31, (1084)" as well as a related notion, only implicit in his proofs. We first develop this within the general framework of the theory of distributive lattices and spectral spaces. Keywords: Constructive mathematics, distributive lattice, Heyting algebra, spectral space, Zariski lattice, Zariski spectrum, Krull dimension, maximal spectrum, Heitmann lattice, Heitmann spectrum, Heitmann dimensions. MSC: 13C15, 03F65, 13A15, 13E05
Chat View PDF

Canonicity and homotopy canonicity for cubical type theory

2022-02-03
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 computationally by induction on … 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 computationally by induction on the type involving several non-canonical choices. We present in this article two canonicity results, both proved by a sconing argument: a homotopy canonicity result, every natural number is path equal to a numeral, even if we take away the equations defining the lifting operation on the type structure, and a canonicity result, which uses these equations in a crucial way. Both proofs are done internally in a presheaf model.
Chat View PDF

Constructive theory of ordinals

2022-01-01
Thierry Coquand , Henri Lombardi , Stefan Neuwirth
In Chapter 3 of his Notes on constructive mathematics, Martin-L{\"o}f describes recursively constructed ordinals. He gives a constructively acceptable version of Kleene's computable ordinals. In fact, the Turing definition of … In Chapter 3 of his Notes on constructive mathematics, Martin-L{\"o}f describes recursively constructed ordinals. He gives a constructively acceptable version of Kleene's computable ordinals. In fact, the Turing definition of computable functions is not needed from a constructive point of view. We give in this paper a constructive theory of ordinals that is similar to Martin-L{\"o}f's theory, but based only on the two relations "$x \leq y$" and "$x < y$", i.e., without considering sequents whose intuitive meaning is a classical disjunction. In our setting, the operation "supremum of ordinals" plays an important r\^ole through its interactions with the relations "$x \leq y$" and "$x < y$". This allows us to approach as much as we may the notion of linear order when the property "$\alpha \leq \beta$ or $\beta \leq \alpha$" is provable only within classical logic. Our aim is to give a formal definition corresponding to intuition, and to prove that our constructive ordinals satisfy constructively all desirable properties. Note that by adding classical logic, we would recover the ordinals of usual classical mathematics, at the cost of a loss of computability for most statements given in the usual form.
Chat View PDF

Controlling unfolding in type theory

2022-01-01
Daniel Gratzer , Jonathan Sterling , Carlo Angiuli +2 more
We present a novel mechanism for controlling the unfolding of definitions in dependent type theory. Traditionally, proof assistants let users specify whether each definition can or cannot be unfolded in … We present a novel mechanism for controlling the unfolding of definitions in dependent type theory. Traditionally, proof assistants let users specify whether each definition can or cannot be unfolded in the remainder of a development; unfolding definitions is often necessary in order to reason about them, but an excess of unfolding can result in brittle proofs and intractably large proof goals. In our system, definitions are by default not unfolded, but users can selectively unfold them in a local manner. We justify our mechanism by means of elaboration to a core type theory with extension types, a connective first introduced in the context of homotopy type theory. We prove a normalization theorem for our core calculus and have implemented our system in the cooltt proof assistant, providing both theoretical and practical evidence for it.
Chat View PDF

Type Theory with Explicit Universe Polymorphism

2022-01-01
Marc Bezem , Thierry Coquand , Peter Dybjer +1 more
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 … 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 explicit constraints between universe levels. We here present a system where we also have products indexed by universe levels and by constraints. Our theory has judgments for internal universe levels, built up from level variables by a successor operation and a binary supremum operation, and also judgments for equality of universe levels.
Chat View PDF

Constructive sheaf models of type theory

2021-10-01
Thierry Coquand , Fabian Ruch , Christian Sattler
Abstract We provide a constructive version of the notion of sheaf models of univalent type theory. We start by relativizing existing constructive models of univalent type theory to presheaves over … Abstract We provide a constructive version of the notion of sheaf models of univalent type theory. We start by relativizing existing constructive models of univalent type theory to presheaves over a base category. Any Grothendieck topology of the base category then gives rise to a family of left-exact modalities, and we recover a model of type theory by localizing the presheaf model with respect to this family of left-exact modalities. We provide then some examples.
Chat View PDF

Formal Topology and Univalent Foundations

2021-07-29
Thierry Coquand , Ayberk Tosun

Syntax and models of Cartesian cubical type theory

2021-04-01
Carlo Angiuli , Guillaume Brunerie , Thierry Coquand +3 more
Abstract We present a cubical type theory based on the Cartesian cube category (faces, degeneracies, symmetries, diagonals, but no connections or reversal) with univalent universes, each containing Π, Σ, path, … Abstract We present a cubical type theory based on the Cartesian cube category (faces, degeneracies, symmetries, diagonals, but no connections or reversal) with univalent universes, each containing Π, Σ, path, identity, natural number, boolean, suspension, and glue (equivalence extension) types. The type theory includes a syntactic description of a uniform Kan operation, along with judgmental equality rules defining the Kan operation on each type. The Kan operation uses both a different set of generating trivial cofibrations and a different set of generating cofibrations than the Cohen, Coquand, Huber, and Mörtberg (CCHM) model. Next, we describe a constructive model of this type theory in Cartesian cubical sets. We give a mechanized proof, using Agda as the internal language of cubical sets in the style introduced by Orton and Pitts, that glue, Π, Σ, path, identity, boolean, natural number, suspension types, and the universe itself are Kan in this model, and that the universe is univalent. An advantage of this formal approach is that our construction can also be interpreted in a range of other models, including cubical sets on the connections cube category and the De Morgan cube category, as used in the CCHM model, and bicubical sets, as used in directed type theory.
Chat View PDF

Regular Entailment Relations

2021-01-01
Thierry Coquand , Henri Lombardi , Stefan Neuwirth
Abstract 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 … Abstract 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. We also describe equivariant systems of ideals à la Lorenzen and show that the remarkable regularisation process he invented yields a regular entailment relation. By providing constructive objects and arguments, we pursue Lorenzen’s aim of “bringing to light the basic, pure concepts in their simple and transparent clarity”.
Chat View PDF

Constructive basic theory of central simple algebras

2021-01-01
Thierry Coquand , Henri Lombardi , Stefan Neuwirth
We provide a constructive treatment of basic results in the theory of central simple algebras. One main issue is the fact that one starting result, Wedderburn's Theorem stating that a … We provide a constructive treatment of basic results in the theory of central simple algebras. One main issue is the fact that one starting result, Wedderburn's Theorem stating that a simple algebra is a matrix algebra over a skew field, is not constructively valid. We solve this problem by proving instead a dynamical version of this theorem. One can use this to give constructive proofs of basic results of the theory of central simple algebras, such as Skolem-Noether Theorem. We illustrate this development by giving an elementary constructive proof of a theorem of Becher (which is itself a consequence of a celebrated theorem of Merkurjev).
Chat View PDF

Reduction Free Normalisation for a proof irrelevant type of propositions

2021-01-01
Thierry Coquand
We show normalisation and decidability of convertibility for a type theory with a hierarchy of universes and a proof irrelevant type of propositions, close to the type system used in … We show normalisation and decidability of convertibility for a type theory with a hierarchy of universes and a proof irrelevant type of propositions, close to the type system used in the proof assistant Lean. Contrary to previous arguments, the proof does not require explicitly to introduce a notion of neutral and normal forms.
Chat View PDF

Lorenzen's proof of consistency for elementary number theory [with an edition and translation of "Ein halbordnungstheoretischer Widerspruchsfreiheitsbeweis'']

2020-06-16
Thierry Coquand , Stefan Neuwirth
We present a manuscript of Paul Lorenzen that provides a proof of consistency for elementary number theory as an application of the construction of the free countably complete pseudocomplemented semilattice … We present a manuscript of Paul Lorenzen that provides a proof of consistency for elementary number theory as an application of the construction of the free countably complete pseudocomplemented semilattice over a preordered set. This manuscript rests in the Oskar-Becker-Nachlass at the Philosophisches Archiv of Universit{a}t Konstanz, file OB 5-3b-5. It has probably been written between March and May 1944. We also compare this proof to Gentzen's and Novikov's, and provide a translation of the manuscript.
Chat View PDF

Lorenzen's Proof of Consistency for Elementary Number Theory

2020-06-12
Thierry Coquand , Stefan Neuwirth
We present a manuscript of Paul Lorenzen that provides a proof of consistency for elementary number theory as an application of the construction of the free countably complete pseudocomplemented semilattice … We present a manuscript of Paul Lorenzen that provides a proof of consistency for elementary number theory as an application of the construction of the free countably complete pseudocomplemented semilattice over a preordered set. This manuscript rests in the Oskar-Becker-Nachlass at the Philosophisches Archiv of Universit{ä}t Konstanz, file OB 5-3b-5. It has probably been written between March and May 1944. We also compare this proof to Gentzen's and Novikov's, and provide a translation of the manuscript.
Chat View PDF

Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality

2020-06-01
Andreas Abel , Thierry Coquand
Normalization fails in type theory with an impredicative universe of propositions and a proof-irrelevant propositional equality. The counterexample to normalization is adapted from Girard's counterexample against normalization of System F … Normalization fails in type theory with an impredicative universe of propositions and a proof-irrelevant propositional equality. The counterexample to normalization is adapted from Girard's counterexample against normalization of System F equipped with a decider for type equality. It refutes Werner's normalization conjecture [LMCS 2008].

A Note on Generalized Algebraic Theories and Categories with Families

2020-01-01
Marc Bezem , Thierry Coquand , Peter Dybjer +1 more
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 structure. … 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 structure. To this end we define inductively how to build a valid signature $Σ$ for a generalized algebraic theory and the associated category of cwfs with a $Σ$-structure and cwf-morphisms that preserve this structure on the nose. Our definition refers to uniform families of contexts, types, and terms, a purely semantic notion. Furthermore, we show how to syntactically construct initial cwfs with $Σ$-structures. This result can be viewed as a generalization of Birkhoff's completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjer's construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of dependent type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a category with families.
Chat View PDF

Constructive sheaf models of type theory

2019-12-22
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 models … 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 models of univalence, that can then be relativized to any presheaf models, and these sheaf models are obtained by localisation for a left exact modality. We provide first an abstract notion of descent data which can be thought of as a higher version of the notion of prenucleus on frames, from which can be generated a nucleus (left exact modality) by transfinite iteration. We then provide several examples.
Chat View PDF

Lattice-ordered groups generated by an ordered group and regular systems of ideals

2019-09-01
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 role in logic (Scott 1974) and in algebra (Lombardi and Quitte … Unbounded entailment relations, introduced by Paul Lorenzen (1951), are a slight variant of a notion which plays a fundamental role in logic (Scott 1974) and in algebra (Lombardi and Quitte 2015). We call systems of ideals their single-conclusion counterpart. If they preserve the order of a commutative ordered monoid $G$ and are equivariant with respect to its law, we call them equivariant systems of ideals for $G$: they describe all morphisms from $G$ to meet-semilattice-ordered monoids generated by (the image of) $G$. Taking a 1953 article by Lorenzen as a starting point, we also describe all morphisms from a commutative ordered group $G$ to lattice-ordered groups generated by $G$ through unbounded entailment relations that preserve its order, are equivariant, and satisfy a regularity property invented by Lorenzen; we call them regular entailment relations. In particular, the free lattice-ordered group generated by $G$ is described through the finest regular entailment relation for $G$, and we provide an explicit description for it; it is order-reflecting if and only if the morphism is injective, so that the Lorenzen-Clifford-Dieudonné theorem fits into our framework. Lorenzen's research in algebra starts as an inquiry into the system of Dedekind ideals for the divisibility group of an integral domain $R$, and specifically into Wolfgang Krull's ``Fundamentalsatz'' that $R$ may be represented as an intersection of valuation rings if and only if $R$ is integrally closed: his constructive substitute for this representation is the regularisation of the system of Dedekind ideals, i.e. the lattice-ordered group generated by it when one proceeds as if its elements are comparable.
Chat View PDF

Homotopy canonicity for cubical type theory

2019-02-18
Thierry Coquand , Simon Huber , Christian Sattler
Chat View PDF

Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality

2019-01-01
Andreas Abel , Thierry Coquand
Normalization fails in type theory with an impredicative universe of propositions and a proof-irrelevant propositional equality. The counterexample to normalization is adapted from Girard's counterexample against normalization of System F … Normalization fails in type theory with an impredicative universe of propositions and a proof-irrelevant propositional equality. The counterexample to normalization is adapted from Girard's counterexample against normalization of System F equipped with a decider for type equality. It refutes Werner's normalization conjecture [LMCS 2008].
Chat View PDF

Regular entailment relations

2019-01-01
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. … 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. We also describe equivariant systems of ideals {\`a} la Lorenzen and show that the remarkable regularisation process invented by him yields a regular entailment relation. By providing constructive objects and arguments, we pursue Lorenzen's aim of "bringing to light the basic, pure concepts in their simple and transparent clarity"
Chat View PDF

Constructive sheaf models of type theory

2019-01-01
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 models … 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 models of univalence, that can then be relativized to any presheaf models, and these sheaf models are obtained by localisation for a left exact modality. We provide first an abstract notion of descent data which can be thought of as a higher version of the notion of prenucleus on frames, from which can be generated a nucleus (left exact modality) by transfinite iteration. We then provide several examples.
Chat View PDF

R\'esolutions libres finies. M\'ethodes constructives

2018-11-05
Thierry Coquand , Henri Lombardi , Claude Quitté +1 more
In this memoir, we give a completely constructive version of the celebrate book 'Finite Free Resolutions' by Northcott, and of some other results related to the depth \`a la Hochster, … In this memoir, we give a completely constructive version of the celebrate book 'Finite Free Resolutions' by Northcott, and of some other results related to the depth \`a la Hochster, the Cayley complexes and their determinants, and the finite projective resolutions.
Chat View PDF

Finite free resolutions. Constructive methods

2018-11-05
Henri Lombardi , Thierry Coquand , Claude Quitté +1 more

Syntactic forcing models for coherent logic

2018-06-28
Marc Bezem , Ulrik Buchholtz , Thierry Coquand
Chat View PDF

On Higher Inductive Types in Cubical Type Theory

2018-06-27
Thierry Coquand , Simon Huber , Anders Mörtberg
Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly … Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. This paper describes a constructive semantics, expressed in a presheaf topos with suitable structure inspired by cubical sets, of some higher inductive types. It also extends cubical type theory by a syntax for the higher inductive types of spheres, torus, suspensions, truncations, and pushouts. All of these types are justified by the semantics and have judgmental computation rules for all constructors, including the higher dimensional ones, and the universes are closed under these type formers.
Chat View PDF

The Univalence Axiom in Cubical Sets

2018-06-26
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 cubical sets as described in Bezem et al. (in: Matthes and Schubert … In this note we show that Voevodsky's univalence axiom holds in the model of type theory based on cubical sets as described in Bezem et al. (in: Matthes and Schubert (eds.) 19th international conference on types for proofs and programs (TYPES 2013), Leibniz international proceedings in informatics (LIPIcs), Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany, vol 26, pp 107–128, 2014. https://doi.org/10.4230/LIPIcs.TYPES.2013.107 . http://drops.dagstuhl.de/opus/volltexte/2014/4628 ) and Huber (A model of type theory in cubical sets. Licentiate thesis, University of Gothenburg, 2015). We will also discuss Swan's construction of the identity type in this variation of cubical sets. This proves that we have a model of type theory supporting dependent products, dependent sums, univalent universes, and identity types with the usual judgmental equality, and this model is formulated in a constructive metatheory.
Chat View PDF

Regular entailment relations

2018-03-08
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. … 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. We also describe equivariant systems of ideals {\`a} la Lorenzen and show that the remarkable regularisation process invented by him yields a regular entailment relation. By providing constructive objects and arguments, we pursue Lorenzen's aim of bringing to light the basic, pure concepts in their simple and transparent clarity
Chat View PDF

On Higher Inductive Types in Cubical Type Theory

2018-02-04
Thierry Coquand , Simon Huber , Anders Mörtberg
Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly … Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. This paper describes a constructive semantics, expressed in a presheaf topos with suitable structure inspired by cubical sets, of some higher inductive types. It also extends cubical type theory by a syntax for the higher inductive types of spheres, torus, suspensions,truncations, and pushouts. All of these types are justified by the semantics and have judgmental computation rules for all constructors, including the higher dimensional ones, and the universes are closed under these type formers.
Chat View PDF

Constructions cachées en algèbre abstraite. Dimension de Krull, Going Up, Going Down

2018-01-01
Henri Lombardi , Thierry Coquand
Nous rappelons des versions \covs de la th\'eorie de la dimension de Krull dans les anneaux commutatifs et dans les \trdisz, dont les bases ont \'et\'e pos\'ees par Joyal, Espan\~ol … Nous rappelons des versions \covs de la th\'eorie de la dimension de Krull dans les anneaux commutatifs et dans les \trdisz, dont les bases ont \'et\'e pos\'ees par Joyal, Espan\~ol et les deux auteurs. Nous montrons sur les exemples de la dimension des alg\`ebres \pfz, du Going Up, du Going Down, % du Principal Ideal Theorem, \ldots que cela nous permet de donner une version \cov des grands th\'eor\`emes classiques, et par cons\'equent de r\'ecup\'erer un contenu calculatoire explicite lorsque ces th\'eor\`emes abstraits sont utilis\'es pour d\'emontrer l'existence d'objets concrets. Nous pensons ainsi mettre en oeuvre une r\'ealisation partielle du programme de Hilbert pour l'alg\`ebre abstraite classique. We present constructive versions of Krull's dimension theory for commutative rings and distributive lattices. The foundations of these constructive versions are due to Joyal, Espan\~ol and the authors. We show that this gives a constructive version of basic classical theorems (dimension of finitely presented algebras, Going up and Going down theorem, \ldots), and hence that we get an explicit computational content where these abstract results are used to show the existence of concrete elements. This can be seen as a partial realisation of Hilbert's program for classical abstract commutative algebra.
Chat View PDF

Canonicity and normalisation for Dependent Type Theory

2018-01-01
Thierry Coquand
We show canonicity and normalization for dependent type theory with a cumulative sequence of universes and a type of Boolean. The argument follows the usual notion of reducibility, going back … We show canonicity and normalization for dependent type theory with a cumulative sequence of universes and a type of Boolean. The argument follows the usual notion of reducibility, going back to Godel's Dialectica interpretation and the work of Tait. A key feature of our approach is the use of a proof relevant notion of reducibility.
Chat View PDF

A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic

2018-01-01
Robin Adams , Marc Bezem , Thierry Coquand
The univalence axiom expresses the principle of extensionality for dependent type theory. How- ever, if we simply add the univalence axiom to type theory, then we lose the property of … The univalence axiom expresses the principle of extensionality for dependent type theory. How- ever, if we simply add the univalence axiom to type theory, then we lose the property of canonicity — that every closed term computes to a canonical form. A computation becomes ‘stuck’ when it reaches the point that it needs to evaluate a proof term that is an application of the univalence axiom. So we wish to find a way to compute with the univalence axiom. While this problem has been solved with the formulation of cubical type theory, where the computations are expressed us- ing a nominal extension of lambda-calculus, it may be interesting to explore alternative solutions, which do not require such an extension. As a first step, we present here a system of propositional higher-order minimal logic (PHOML). There are three kinds of typing judgement in PHOML. There are terms which inhabit types, which are the simple types over Ω. There are proofs which inhabit propositions, which are the terms of type Ω. The canonical propositions are those constructed from ⊥ by implication ⊃. Thirdly, there are paths which inhabit equations M = A N , where M and N are terms of type A. There are two ways to prove an equality: reflexivity, and propositional extensionality — logically equivalent propositions are equal. This system allows for some definitional equalities that are not present in cubical type theory, namely that transport along the trivial path is identity. We present a call-by-name reduction relation for this system, and prove that the system satisfies canonicity: every closed typable term head-reduces to a canonical form. This work has been formalised in Agda.
Chat View PDF

Résolutions libres finies. Méthodes constructives

2018-01-01
Thierry Coquand , Henri Lombardi , Claude Quitté +1 more
In this memoir, we give a completely constructive version of the celebrate book 'Finite Free Resolutions' by Northcott, and of some other results related to the depth à la Hochster, … In this memoir, we give a completely constructive version of the celebrate book 'Finite Free Resolutions' by Northcott, and of some other results related to the depth à la Hochster, the Cayley complexes and their determinants, and the finite projective resolutions.
Chat View PDF

Hidden constructions in abstract algebra. Krull Dimension of distributive lattices and commutative rings

2018-01-01
Thierry Coquand , Henri Lombardi
We present constructive versions of Krull's dimension theory for commutative rings and distributive lattices. The foundations of these constructive versions are due to Joyal, Español and the authors. We show … We present constructive versions of Krull's dimension theory for commutative rings and distributive lattices. The foundations of these constructive versions are due to Joyal, Español and the authors. We show that the notion of Krull dimension has an explicit computational content in the form of existence (or lack of existence) of some algebraic identities. We can then get an explicit computational content where abstract results about dimensions are used to show the existence of concrete elements. This can be seen as a partial realisation of Hilbert's program for classical abstract commutative algebra.
Chat View PDF

On Higher Inductive Types in Cubical Type Theory

2018-01-01
Thierry Coquand , Simon Huber , Anders Mörtberg
Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly … Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. This paper describes a constructive semantics, expressed in a presheaf topos with suitable structure inspired by cubical sets, of some higher inductive types. It also extends cubical type theory by a syntax for the higher inductive types of spheres, torus, suspensions,truncations, and pushouts. All of these types are justified by the semantics and have judgmental computation rules for all constructors, including the higher dimensional ones, and the universes are closed under these type formers.
Chat View PDF

Constructions cachées en algèbre abstraite. Dimension de Krull, Going Up, Going Down

2018-01-01
Henri Lombardi , Thierry Coquand
Chat View PDF

Syntactic Forcing Models for Coherent Logic

2017-12-20
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 not … 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 not presuppose that the logic has equality. As an application we give a coherent theory T and a sentence {\psi} which is T-redundant (for any geometric implication {\phi}, possibly with equality, if T + {\psi} proves {\phi}, then T proves {\phi}), yet false in the generic model of T. This answers in the negative a question by Wraith.
Chat View PDF

An elementary proof of Wiebe's Theorem

2017-12-14
Thierry Coquand , Claire Tête

Hidden constructions in abstract algebra, Krull Dimension, Going Up, Going Down

2017-12-13
Thierry Coquand , Henri Lombardi
We present constructive versions of Krull's dimension theory for commutative rings and distributive lattices. The foundations of these constructive versions are due to Joyal, Espanol and the authors. We show … We present constructive versions of Krull's dimension theory for commutative rings and distributive lattices. The foundations of these constructive versions are due to Joyal, Espanol and the authors. We show that this gives a constructive version of basic classical theorems (dimension of finitely presented algebras, Going up and Going down theorem, \ldots), and hence that we get an explicit computational content where these abstract results are used to show the existence of concrete elements. This can be seen as a partial realisation of Hilbert's program for classical abstract commutative algebra.

Common Coauthors

Coauthor Papers Together
Henri Lombardi 40
Stefan Neuwirth 14
Marc Bezem 14
Simon Huber 12
Anders Mörtberg 10
Bas Spitters 10
Claude Quitté 9
Bassel Mannaa 7
Christian Sattler 6
Martı́n Hötzel Escardó 6
Vincent Siles 5
Peter Schuster 5
Fabian Ruch 5
Thorsten Altenkirch 5
Nicolai Kraus 4
Cyril Cohen 4
Andreas Abel 4
Claire Tête 4
Ulrik Buchholtz 3
Jónathan Heras 3
Arnaud Spiwack 3
Felix Cherubini 3
Carlo Angiuli 3
Erik Palmgren 3
Robin Adams 3
Matthias Hutzler 3
Peter Dybjer 3
Emily Riehl 2
Daniel R. Licata 2
Bruno Barras 2
Guillaume Brunerie 2
Miguel Pagano 2
Alban Quadrat 2
Kuen-Bang Hou 2
Henrik Persson 2
Robert Harper 2
Steve Awodey 2
Peter LeFanu Lumsdaine 1
Ihsen Yengui 1
Richard Garner 1
Felix Cherubini 1
Per Martin-Löf 1
Eric Finster 1
Claude Quitt� 1
Lionel Ducos 1
Ayberk Tosun 1
Benno van den Berg 1
Erik Parmann 1
Jonathan Sterling 1
M Bezem 1

Commonly Cited References

A Course in Constructive Algebra

1988-01-01
Ray Mines , Fred Richman , Wim Ruitenburg

Dynamical method in algebra: effective Nullstellensätze

2001-08-01
Michel Coste , Henri Lombardi , Marie-Françoise Roy
Chat View PDF

Homotopy theoretic models of identity types

2008-07-14
Steve Awodey , Michael A. Warren
This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing … This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing the Hofmann-Streicher groupoid model of Martin-Loef type theory.
Chat View PDF

Commutative Algebra: Constructive Methods

2015-01-01
Henri Lombardi , Claude Quitté
Chat View PDF

Abstrakte Begründung der multiplikativen Idealtheorie

1939-12-01
P. Lorenzen

An intuitionistic theory of types

1998-10-15
Per Martin-Löf
The theory of types with which we shall be concerned is intended to be a full scale system for formalizing intuitionistic mathematics as developed, for example, in the book by … The theory of types with which we shall be concerned is intended to be a full scale system for formalizing intuitionistic mathematics as developed, for example, in the book by Bishop 1967. The language of the theory is richer than the language of first order predicate logic. This makes it possible to strengthen the axioms for existence and disjunction. In the case of existence, the possibility of strengthening the usual elimination rule seems first to have been indicated by Howard 1969, whose proposed axioms are special cases of the existential elimination rule of the present theory. Furthermore, there is a reflection principle which links the generation of objects and types and plays somewhat the same role for the present theory as does the replacement axiom for Zermelo-Fraenkel set theory. An earlier, not yet conclusive, attempt at formulating a theory of this kind was made by Scott 1970. Also related, although less closely, are the type and logic free theories of constructions of Kreisel 1962 and 1965 and Goodman 1970. In its first version, the present theory was based on the strongly impredicative axiom that there is a type of all types whatsoever, which is at the same time a type and an object of that type. This axiom had to be abandoned, however, after it was shown to lead to a contradiction by Jean Yves Girard. I am very grateful to him for showing me his paradox. The change that it necessitated is so drastic that my theory no longer contains intuitionistic simple type theory as it originally did. Instead, its proof theoretic strength should be close to that of predicative analysis. Mathematical objects and their types. We shall think of mathematical objects or constructions. Every mathematical object is of a certain kind or type. Better, a mathematical object is always given together with its type, that is, it is not just an object, it is an object of a certain type.

Algebraische und logistische Untersuchungen über freie Verbände

1951-06-01
Paul Lorenzen
Die Verbandstheorie ist bekanntlich von Dedekind an Hand seiner idealtheoretischen Untersuchungen begründet worden. Es hat sich in letzter Zeit herausgestellt, daß die wesentliche Eigenschaft des Dedekind'schen Idealsystems darin liegt, daß … Die Verbandstheorie ist bekanntlich von Dedekind an Hand seiner idealtheoretischen Untersuchungen begründet worden. Es hat sich in letzter Zeit herausgestellt, daß die wesentliche Eigenschaft des Dedekind'schen Idealsystems darin liegt, daß die Ideale einen Halbverband (§1) bilden. Die Idealtheorie führt so auf die Frage nach alien Halbverbänden über einer beliebigen halbgeordneten Menge M. Die einfache Antwort enthält §2. Ebenso einfach ist die Frage nach alien distributiven Verbänden uber M zu beantworten. In beiden Fällen ist unter den Halbverbänden bzw. distributiven Verbänden über M einer dadurch ausgezeichnet, daß alle anderen homomorph zu ihm sind. Diesen ausgezeichneten Halbverband bzw. distributiven Verband nennen wir den freien Halbverband bzw. freien distributiven Verband über M . Zu neuen Fragen kommt man bei der Untersuchung speziellerer Halbverbände über M . Es ist z.B. bekannt, daß M stets zu einem vollständigen Boole'schen Verband erweitert werden kann. Gibt es unter diesen Erweiterungen stets den freien vollständigen Boole'schen Verband über M , der dadurch ausgezeichnet ist, daß alle anderen zu ihm homomorph sind ? In §3 wird zunächst die Existenz des freien orthokomplementären Halbverbandes über M bewiesen. Mit Hilfe der hier benutzten Methode läßt sich auch der Existenzbeweis für den freien abzählbar-vollständigen Boole'schen Verband über M führen.

Generating non-Noetherian modules constructively

2004-11-10
Thierry Coquand , Henri Lombardi , Claude Quitt�

Théorie algorithmique des anneaux arithmétiques, des anneaux de Prüfer et des anneaux de Dedekind

2004-09-17
Lionel Ducos , Henri Lombardi , Claude Quitté +1 more

Internal type theory

1996-01-01
Peter Dybjer

Homotopy Type Theory: Univalent Foundations of Mathematics

2013-01-01
Peter Aczel , Benedikt Ahrens , Thorsten Altenkirch +7 more
Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of … Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.
Chat View PDF

Cubical Type Theory: a constructive interpretation of the univalence axiom

2015-05-18
Cyril Cohen , Thierry Coquand , Simon Huber +1 more
This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in … This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.
Chat View PDF

Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems

2005-12-28
Thierry Coquand , Bas Spitters
We present a constructive proof of the Stone-Yosida representation theorem for Riesz spaces motivated by considerations from formal topology. This theorem is used to derive a representation theorem for f-algebras. … We present a constructive proof of the Stone-Yosida representation theorem for Riesz spaces motivated by considerations from formal topology. This theorem is used to derive a representation theorem for f-algebras. In turn, this theorem implies the Gelfand representation theorem for C*-algebras of operators on Hilbert spaces as formulated by Bishop and Bridges. Our proof is shorter, clearer, and we avoid the use of approximate eigenvalues.
Chat View PDF

About Stone's notion of spectrum

2004-10-05
Thierry Coquand

Constructive Krull dimension of lattices

1982-01-01
Luis Español González

The fundamental theorem of algebra: a constructive development without choice

2000-11-01
Fred Richman
Is it reasonable to do constructive mathematics without the axiom of countable choice?Serious schools of constructive mathematics all assume it one way or another, but the arguments for it are … Is it reasonable to do constructive mathematics without the axiom of countable choice?Serious schools of constructive mathematics all assume it one way or another, but the arguments for it are not compelling.The fundamental theorem of algebra will serve as an example of where countable choice comes into play and how to proceed in its absence.Along the way, a notion of a complete metric space, suitable for a choiceless environment, is developed.
Chat View PDF

Dimension de Krull, Nullstellensätze et évaluation dynamique

2002-02-01
Henri Lombardi
Chat View PDF

A model of type theory in cubical sets

2014-01-01
M Bezem , Thierry Coquand , Simon Huber
We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types … We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types into an equality. We also explain how to model propositional truncation and the circle. While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky's Univalence Axiom.

Über halbgeordnete Gruppen

1950-12-01
Paul Lorenzen

A globalization of the Hahn-Banach theorem

1991-09-01
Christopher J. Mulvey , Joan Wick Pelletier

STONE SPACES (Cambridge Studies in Advanced Mathematics 3)

1987-03-01
John Bell
By Peter T. Johnstone: pp. 370. £12.95; US$24.95. (Cambridge University Press, 1986.) By Peter T. Johnstone: pp. 370. £12.95; US$24.95. (Cambridge University Press, 1986.)

AN ELEMENTARY CHARACTERIZATION OF KRULL DIMENSION

2005-10-06
Thierry Coquand Henri Lombardi , Marie-Françoise Roy
Abstract This chapter contributes to the new direction in constructive algebra originated by Coquand, Lombardi, and others, which aims at a partial realisation of Hilbert's programme. The idea is to … Abstract This chapter contributes to the new direction in constructive algebra originated by Coquand, Lombardi, and others, which aims at a partial realisation of Hilbert's programme. The idea is to prove that theorems in commutative algebra constructively, and at the same low type level at which they can be formulated. To this end, the chapter needs to reduce the complexity of some concepts, in the present case that of Krull dimension of a commutative ring. Although the traditional definition of it seems quite intuitive, it requires quantifying over all prime ideals of the given ring. To circumvent this problem the chapter gives an inductive characterization of Krull dimension, without primes, which carries over to this setting the inductive concept of dimension going back to Brouwer, Menger, and Urysohn. This follows the geometrical intuition that an algebraic variety is of dimension ≤ k if and only if each subvariety has a boundary of dimension &amp;lt; k.

The Equivalence Extension Property and Model Structures

2017-01-01
Christian Sattler
We give an elementary construction of a certain class of model structures. In particular, we rederive the Kan model structure on simplicial sets without the use of topological spaces, minimal … We give an elementary construction of a certain class of model structures. In particular, we rederive the Kan model structure on simplicial sets without the use of topological spaces, minimal complexes, or any concrete model of fibrant replacement such as Kan's Ex^infinity functor. Our argument makes crucial use of the glueing construction developed by Cohen et al. in the specific setting of certain cubical sets.
Chat View PDF

La logique des topos

1981-03-01
André Boileau , André Joyal
Les synthèses nouvelles par le rapprochement de disciplines mathématiques différentes constituent des événements remarquables dans l'histoire des mathématiques. Une telle synthèse semble émerger actuellement du rapprochement de: (1) La géométrie … Les synthèses nouvelles par le rapprochement de disciplines mathématiques différentes constituent des événements remarquables dans l'histoire des mathématiques. Une telle synthèse semble émerger actuellement du rapprochement de: (1) La géométrie algébrique sous la forme élaborée par Grothendieck. (2) La logique formelle. Le point de contact s'est effectué aux environs de 1970 par W. Lawvere et M. Tierney et l'instrument de rapprochement a été la théorie des catégories, plus particulièrement la théorie des faisceaux. Depuis ce moment, une dialectique incessante imprime un mouvement dynamique à toute une série de recherches qui visent à rapprocher les méthodes suivantes: (1) Mathématique intuitionniste. (2) Forcing de Cohen et Robinson. (3) Logique algébrique. (4) Géométrie algébrique. (5) Géométrie différentielle et analytique. (6) Topologie algébrique: cohomologie, homotopie. (7) Théorie de Galois. Certains rapprochements sont dans un stade avancé, d'autres encore embryonnaires: (6) ↔ (3). La structure centrale qui joue le rôle d'élément provocateur et unificateur est celle de topos. Avant d'être axiomatisée par Lawvere, celle-ci a été étudiée systématiquement par l'école de Grothendieck (voir [1]) et c'est dans le contexte de la géométrie algébrique qu'elle fit son apparition. Dans cet article nous utiliserons cependant la définition de Lawvere telle qu'améliorée par Mikkelsen [12] et Kock [8]. Le but de ce travail est de présenter une version (au sens de la logique formelle) du concept de topos et d'examiner brièvement les rapports entre la théorie des topos, la logique et les mathématiques. Cette version a déjà été exposée par l'un des auteurs lors du Séminaire de Mathématiques Supérieures de l'Université de Montréal, à l'été 1974. Depuis elle a fait l'objet d'une thèse où elle a été améliorée et sa cohérence vérifiée [2]. Des systèmes différents ont été proposés simultanément par Fourman [4] et Coste [3].

An algebraic weak factorisation system on 01-substitution sets: a constructive proof

2016-01-01
Andrew Swan
We will construct an algebraic weak factorisation system on the category of 01 substitution sets such that the R-algebras are precisely the Kan fibrations together with a choice of Kan … We will construct an algebraic weak factorisation system on the category of 01 substitution sets such that the R-algebras are precisely the Kan fibrations together with a choice of Kan filling operation. The proof is based on Garner's small object argument for algebraic weak factorization systems. In order to ensure the proof is valid constructively, rather than applying the general small object argument, we give a direct proof based on the same ideas. We use this us to give an explanation why the J computation rule is absent from the original cubical set model and suggest a way to fix this.
Chat View PDF

Sur un théorème de Kronecker concernant les variétés algébriques

2004-01-20
Thierry Coquand
Chat View PDF

Hidden Constructions in Abstract Algebra: Krull Dimension of Distributive Lattices and Commutative Rings

2017-07-27
Thierry Coquand , Henri Lombardi
Since the circulation, in 1974, of the first draft of "The construction D + XDS [X], J. Algebra 53 (1978), 423–439" a number of variations of this construction have appeared. … Since the circulation, in 1974, of the first draft of "The construction D + XDS [X], J. Algebra 53 (1978), 423–439" a number of variations of this construction have appeared. Some of these are: The generalized D + M construction, the A + (X)B[X] construction, with X a single variable or a set of variables, and the D + I construction (with I not necessarily prime). These constructions have proved their worth not only in providing numerous examples and counter examples in commutative ring theory, but also in providing statements that often turn out to be forerunners of results on general pullbacks. The aim of this paper will be to discuss these constructions and the remarkable uses they have been put to. I will concentrate more on the A + XB[X] construction, its basic properties and examples arising from it.
Chat View PDF

On Higher Inductive Types in Cubical Type Theory

2018-06-27
Thierry Coquand , Simon Huber , Anders Mörtberg
Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly … Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. This paper describes a constructive semantics, expressed in a presheaf topos with suitable structure inspired by cubical sets, of some higher inductive types. It also extends cubical type theory by a syntax for the higher inductive types of spheres, torus, suspensions, truncations, and pushouts. All of these types are justified by the semantics and have judgmental computation rules for all constructors, including the higher dimensional ones, and the universes are closed under these type formers.
Chat View PDF

Valuations and Dedekind's Prague Theorem

2001-01-01
Thierry Coquand , Henrik Persson

Axioms for Modelling Cubical Type Theory in a Topos

2016-08-25
Ian Orton , Andrew M. Pitts
The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an interval-like object I in a topos to give a model … The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an interval-like object I in a topos to give a model of type theory in which elements of identity types are functions with domain I. Cohen, Coquand, Huber and Mortberg give such a model using a particular category of presheaves. We investigate the extent to which their model construction can be expressed in the internal type theory of any topos and identify a collection of quite weak axioms for this purpose. This clarifies the definition and properties of the notion of uniform Kan filling that lies at the heart of their constructive interpretation of Voevodsky's univalence axiom. Furthermore, since our axioms can be satisfied in a number of different ways, we show that there is a range of topos-theoretic models of homotopy type theory in this style.
Chat View PDF

The equivalence axiom and univalent models of type theory. (Talk at CMU on February 4, 2010)

2014-01-01
Vladimir Voevodsky
This is the text of my talk at CMU on Feb. 4, 2010 were I gave the second public presentation of the Univalence Axiom (called "equivalence axiom" in the text). … This is the text of my talk at CMU on Feb. 4, 2010 were I gave the second public presentation of the Univalence Axiom (called "equivalence axiom" in the text). The first presentation of the axiom was in a lecture at LMU Munich in November 2009.
Chat View PDF

An experimental library of formalized Mathematics based on the univalent foundations

2015-01-20
Vladimir Voevodsky
This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started … This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started to work on this library in February 2010 in order to gain experience with formalization of Mathematics in a constructive type theory based on the intuition gained from the univalent models (see Kapulkin et al. 2012).
Chat View PDF

THE SIMPLICIAL MODEL OF UNIVALENT FOUNDATIONS

2014-01-01
Krzysztof Kapulkin , Peter LeFanu Lumsdaine , Vladimir Voevodsky
In this paper, we construct and investigate a model of the Univalent Foundations of Mathematics in the category of simplicial sets. To this end, we rst give a new technique … In this paper, we construct and investigate a model of the Univalent Foundations of Mathematics in the category of simplicial sets. To this end, we rst give a new technique for constructing models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan bration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in our model. As a corollary, we conclude that Univalent Foundations are at least as consistent as ZFC with two inaccessible cardinals.
Chat View PDF

Sheaves in Geometry and Logic

1994-01-01
Saunders Mac Lane , Ieke Moerdijk

Proof theory in the USSR 1925–1969

1991-06-01
Grigori Mint︠s︡
Abstract We present a survey of proof theory in the USSR beginning with the paper by Kolmogorov [1925] and ending (mostly) in 1969; the last two sections deal with work … Abstract We present a survey of proof theory in the USSR beginning with the paper by Kolmogorov [1925] and ending (mostly) in 1969; the last two sections deal with work done by A. A. Markov and N. A. Shanin in the early seventies, providing a kind of effective interpretation of negative arithmetic formulas. The material is arranged in chronological order and subdivided according to topics of investigation. The exposition is more detailed when the work is little known in the West or the original presentation can be improved using notions or results which appeared later. This includes such topics as Novikov's cut-elimination method (regular formulas) and Maslov's inverse method for the predicate logic.

A nilregular element property

2005-07-01
Thierry Coquand , Henri Lombardi , Peter Schuster
Chat View PDF

Partial Horn logic and cartesian categories

2006-11-21
Erik Palmgren , Steve Vickers

Univalence for inverse diagrams and homotopy canonicity

2014-11-24
Michael Shulman
We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory … We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory on inverse diagrams, and relies on the fact that Reedy fibrant diagrams correspond to contexts of a certain shape in type theory. This has two main applications. First, by considering inverse diagrams in Voevodsky's univalent model in simplicial sets, we obtain new models of univalence in a number of (∞, 1)-toposes; this answers a question raised at the Oberwolfach workshop on homotopical type theory. Second, by gluing the syntactic category of univalent type theory along its global sections functor to groupoids, we obtain a partial answer to Voevodsky's homotopy-canonicity conjecture: in 1-truncated type theory with one univalent universe of sets, any closed term of natural number type is homotopic to a numeral.
Chat View PDF

CONSTRUCTIVE KRULL DIMENSION I: INTEGRAL EXTENSIONS

2009-02-01
Thierry Coquand , Lionel Ducos , Henri Lombardi +1 more
We give a constructive approach to the well known classical theorem saying that an integral extension doesn't change the Krull dimension. We give a constructive approach to the well known classical theorem saying that an integral extension doesn't change the Krull dimension.

Some points in formal topology

2003-07-22
Giovanni Sambin

Dynamic Newton–Puiseux theorem

2013-01-01
Bassel Mannaa , Thierry Coquand
A constructive version of Newton-Puiseux theorem for computing the Puiseux expansions of algebraic curves is presented.The proof is based on a classical proof by Abhyankar.Algebraic numbers are evaluated dynamically; hence … A constructive version of Newton-Puiseux theorem for computing the Puiseux expansions of algebraic curves is presented.The proof is based on a classical proof by Abhyankar.Algebraic numbers are evaluated dynamically; hence the base field need not be algebraically closed and a factorization algorithm of polynomials over the base field is not needed.The extensions obtained are a type of regular algebras over the base field and the expansions are given as formal power series over these algebras.
Chat View PDF

Pointers in Recursion: Exploring the Tropics

2019-12-16
Paulin Jacobé de Naurois
We translate the usual class of partial/primitive recursive functions to a pointer recursion framework, accessing actual input values via a pointer reading unit-cost function. These pointer recursive functions classes are … We translate the usual class of partial/primitive recursive functions to a pointer recursion framework, accessing actual input values via a pointer reading unit-cost function. These pointer recursive functions classes are proven equivalent to the usual partial/primitive recursive functions. Complexity-wise, this framework captures in a streamlined way most of the relevant sub-polynomial classes. Pointer recursion with the safe/normal tiering discipline of Bellantoni and Cook corresponds to polylogtime computation. We introduce a new, non-size increasing tiering discipline, called tropical tiering. Tropical tiering and pointer recursion, used with some of the most common recursion schemes, capture the classes logspace, logspace/polylogtime, ptime, and NC. Finally, in a fashion reminiscent of the safe recursive functions, tropical tier-ing is expressed directly in the syntax of the function algebras, yielding the tropical recursive function algebras.
Chat View PDF

Notes on Gelfand’s Theory

1967-01-01
N.G. de Bruijn , W. Van Der Meiden

Der erste Widerspruchsfreiheitsbeweis für die klassische Zahlentheorie

1974-08-01
Gerhard Gentzen

The Simplicial Model of Univalent Foundations (after Voevodsky)

2012-11-12
Chris Kapulkin , Peter LeFanu Lumsdaine
We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models … We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan fibration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in our model. As a corollary, we conclude that Martin-Lof type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals.
Chat View PDF

Generating modules efficiently: Theorems from algebraic K-theory

1973-11-01
David Eisenbud , E. Graham Evans

ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

1958-12-01
Von Kurt Gödel
Zusammenfassung P. Bernays hat darauf hingewiesen, dass man, um die Widerspruchs freiheit der klassischen Zahlentheorie zu beweisen, den Hilbertschen flniter Standpunkt dadurch erweitern muss, dass man neben den auf Symbole … Zusammenfassung P. Bernays hat darauf hingewiesen, dass man, um die Widerspruchs freiheit der klassischen Zahlentheorie zu beweisen, den Hilbertschen flniter Standpunkt dadurch erweitern muss, dass man neben den auf Symbole sich beziehenden kombinatorischen Begriffen gewisse abstrakte Begriffe zulässt, Die abstrakten Begriffe, die bisher für diesen Zweck verwendet wurden, sinc die der konstruktiven Ordinalzahltheorie und die der intuitionistischer. Logik. Es wird gezeigt, dass man statt deesen den Begriff einer berechenbaren Funktion endlichen einfachen Typs über den natürlichen Zahler benutzen kann, wobei keine anderen Konstruktionsverfahren für solche Funktionen nötig sind, als einfache Rekursion nach einer Zahlvariablen und Einsetzung von Funktionen ineinander (mit trivialen Funktionen als Ausgangspunkt). Abstract P. Bernays has pointed out that, in order to prove the consistency of classical number theory, it is necessary to extend Hilbert's finitary stand-point by admitting certain abstract concepts in addition to the combinatorial concepts referring to symbols. The abstract concepts that so far have been used for this purpose are those of the constructive theory of ordinals and those of intuitionistic logic. It is shown that the concept of a computable function of finite simple type over the integers can be used instead, where no other procedures of constructing such functions are necessary except simple recursion by an integral variable and substitution of functions in each other (starting with trivial functions).
Chat View PDF

Die grundlagen der mathematik

1928-12-01
David Hilbert
Chat View PDF

The spectral theory of commutative C<sup>∗</sup>-algebras: The constructive spectrum

2000-12-01
Bernhard Banaschewski , Christopher J. Mulvey
This paper introduces the notion of a commutative C∗-algebra in a Grothendieck topos E and subsequently that of the spectrum MFn A of A, presented as the locale determined by … This paper introduces the notion of a commutative C∗-algebra in a Grothendieck topos E and subsequently that of the spectrum MFn A of A, presented as the locale determined by an appropriate propositional theory in the topos E which describes the basic properties of a multplicative linear functional on A. Further, the locale CE of complex numbers in the topos E is defined in a similar manner and some of its basic properties are established, such as its complete regularity and the compactness of the unit square in CE. Finally, it is shown that the locale MFn A is compact and completely regular, extending the classical result that the multiplicative linear functionals on a commutative C∗-algebra form a compact Hausdorff space in the weak∗ topology.

Minimal invariant spaces in formal topology

1997-09-01
Thierry Coquand
A standard result in topological dynamics is the existence of minimal subsystem. It is a direct consequence of Zorn's lemma: given a compact topological space X with a map f … A standard result in topological dynamics is the existence of minimal subsystem. It is a direct consequence of Zorn's lemma: given a compact topological space X with a map f : X → X , the set of compact non empty subspaces K of X such that f(K) ⊆ K ordered by inclusion is inductive, and hence has minimal elements. It is natural to ask for a point-free (or formal) formulation of this statement. In a previous work [3], we gave such a formulation for a quite special instance of this statement, which is used in proving a purely combinatorial theorem (van de Waerden's theorem on arithmetical progression). In this paper, we extend our analysis to the case where X is a boolean space, that is compact totally disconnected. In such a case, we give a point-free formulation of the existence of a minimal subspace for any continuous map f : X → X . We show that such minimal subspaces can be described as points of a suitable formal topology, and the “existence” of such points become the problem of the consistency of the theory describing a generic point of this space. We show the consistency of this theory by building effectively and algebraically a topological model. As an application, we get a new, purely algebraic proof, of the minimal property of [3]. We show then in detail how this property can be used to give a proof of (a special case of) van der Waerden's theorem on arithmetical progression, that is “similar in structure” to the topological proof [6, 8], but which uses a simple algebraic remark (Proposition 1) instead of Zorn's lemma. A last section tries to place this work in a wider context, as a reformulation of Hilbert's method of introduction/elimination of ideal elements.