arXiv subjects

Thierry Coquand

Publications and source records attributed to Thierry Coquand.

At least 55 records · Page 3Linked to original sources

arXiv2018

On Higher Inductive Types in Cubical Type Theory

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.

cs.LO↗

arXiv2018

Constructions cachées en algèbre abstraite. Dimension de Krull, Going Up, Going Down (revised version, 2008)

Nous rappelons des versions constructives de la théorie de la dimension de Krull dans les anneaux commutatifs et dans les treillis distributifs, dont les bases ont été posées par Joyal, Espanõl et les deux auteurs. Nous montrons sur les exemples de la dimension des algèbres de présentation finie, du Going Up, du Going Down \ldots que cela nous permet de donner une version constructive de grands théorèmes classiques, et par conséquent de récupérer un contenu calculatoire explicite lorsque ces théorèmes abstraits sont utilisés pour démontrer l'existence d'objets concrets. Nous pensons ainsi mettre en oeuvre une réalisation partielle du programme de Hilbert pour l'algèbre 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õl 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 when 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.

math.AC↗

arXiv2017

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

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.

math.AC↗

arXiv2017

Syntactic Forcing Models for Coherent Logic

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 ψ which is T-redundant (for any geometric implication ϕ, possibly with equality, if T + ψ proves ϕ, then T proves ϕ), yet false in the generic model of T. This answers in the negative a question by Wraith.

math.LO↗

arXiv2017

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

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õl 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.

math.AC↗

arXiv2017

The univalence axiom in cubical sets

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 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.

math.LO↗

arXiv2017

The Independence of Markov's Principle in Type Theory

In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One way to prove this would be to remark that Markov's principle does not hold in a sheaf model of type theory over Cantor space, since Markov's principle does not hold for the generic point of this model. Instead we design an extension of type theory, which intuitively extends type theory by the addition of a generic point of Cantor space. We then show the consistency of this extension by a normalization argument. Markov's principle does not hold in this extension, and it follows that it cannot be proved in type theory.

cs.LO↗

arXiv2017

Stack Semantics of Type Theory

We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalising the groupoid model of type theory. As an application, we show that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation.

cs.LO↗

arXiv2017

Notions of Anonymous Existence in Martin-Löf Type Theory

As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-Löf type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have unique identity proofs. A key ingredient in these constructions are weakly constant endofunctions on identity types. We study such endofunctions on arbitrary types and show that they always factor through a propositional type, the truncated or squashed domain. Such a factorization is impossible for weakly constant functions in general (a result by Shulman), but we present several non-trivial cases in which it can be done. Based on these results, we define a new notion of anonymous existence in type theory and compare different forms of existence carefully. In addition, we show possibly surprising consequences of the judgmental computation rule of the truncation, in particular in the context of homotopy type theory. All the results have been formalized and verified in the dependently typed programming language Agda.

cs.LO↗

arXiv2017

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

The univalence axiom expresses the principle of extensionality for dependent type theory. However, 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 using 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 $\bot$ by implication $\supset$. 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.

cs.LO↗

arXiv2016

Cubical Type Theory: a constructive interpretation of the univalence axiom

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.

cs.LO↗

arXiv2014

A Sheaf Model of the Algebraic Closure

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 of K. We give a possible constructive interpretation of the existence of the algebraic closure of a field in characteristic 0 by building, in a constructive metatheory, a suitable site model where there is such an algebraic closure. One can then extract computational content from this model. We give examples of computation based on this model.

math.LO↗

arXiv2013

Dynamic Newton-Puiseux Theorem

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.

math.AC↗

arXiv2012

A constructive proof of Simpson's Rule

For most purposes, one can replace the use of Rolle's theorem and the mean value theorem, which are not constructively valid, by the law of bounded change. The proof of two basic results in numerical analysis, the error term for Lagrange interpolation and Simpson's rule, however seem to require the full strength of the classical Rolle's Theorem. The goal of this note is to justify these two results constructively, using ideas going back to Ampère and Genocchi.

math.NA↗

arXiv2012

Computing Persistent Homology within Coq/SSReflect

Persistent homology is one of the most active branches of Computational Algebraic Topology with applications in several contexts such as optical character recognition or analysis of point cloud data. In this paper, we report on the formal development of certified programs to compute persistent Betti numbers, an instrumental tool of persistent homology, using the Coq proof assistant together with the SSReflect extension. To this aim it has been necessary to formalize the underlying mathematical theory of these algorithms. This is another example showing that interactive theorem provers have reached a point where they are mature enough to tackle the formalization of nontrivial mathematical theories.

cs.LO↗

arXiv2011

A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance

We define a logical framework with singleton types and one universe of small types. We give the semantics using a PER model; it is used for constructing a normalisation-by-evaluation algorithm. We prove completeness and soundness of the algorithm; and get as a corollary the injectivity of type constructors. Then we give the definition of a correct and complete type-checking algorithm for terms in normal form. We extend the results to proof-irrelevant propositions.

cs.LO↗

arXiv2010

Constructive Theory of Banach algebras

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 proofs of Wiener's result on the inverse of Fourier series and Wiener's Tauberian Theorem, in a sequel to this paper we show how this can be used in a localic, or point-free, description of the spectrum of a Banach algebra.

math.LO↗

arXiv2009

Metric complements of overt closed sets

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, compact, then its collection of points is Bishop compact.

math.LO↗