There have recently been several developments in synthetic mathematics using extensions of dependent type theory with univalence and higher inductive types: simplicial homotopy type theory, synthetic algebraic geometry and synthetic Stone duality. We provide a foundation of higher sheaf models of type theory in a constructive metatheory and, in particular, build constructive models of these formal systems.

Abstract We present a new way to control the unfolding of definitions in dependent type theory. Traditionally, proof assistants require users to fix whether each definition will or will not 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 theory with extension types – a connective first introduced in the context of homotopy type theory – and by establishing a normalization theorem for our core calculus. We have implemented controlled unfolding in the proof assistant, inspiring an independent implementation in Agda.

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.

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.

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.

We solve in polynomial time two decision problems that occur in type checking when typings depend on universe level constraints.

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.

Abstract We give a syntax independent formulation of finitely presented generalized algebraic theories as initial objects in categories of categories with families (cwfs) with extra structure. To this end, we simultaneously define the notion of a presentation Σ of a generalized algebraic theory and the associated category CwFΣ of small cwfs with a Σ-structure and cwf-morphisms that preserve Σ-structure on the nose. Our definition refers to the purely semantic notion of uniform family of contexts, types, and terms in CwFΣ. Furthermore, we show how to syntactically construct an initial cwf with a Σ-structure. 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 Martin-Löf type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a small category with families. Finally, we show how to extend our definition to some generalized algebraic theories that are not finitely presented, such as the theory of contextual cwfs.

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.

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

We give a constructive proof of Skolem’s Theorem for coherent logic and discuss several applications, including a negative answer to a question by Wraith.

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.

We present a domain model of dependent type theory and use it to prove basic metatheoretic properties. In particular, we prove that two convertible terms have the same Böhm tree. The method used is reminiscent of the use of “inclusive predicates” in domain theory.

We present a simple inner model construction for dependent type theory, which preserves univalence.

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.

We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing 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.

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.

The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. It is presented during the annual conference of the EACSL (CSL'xx). This contribution reports on the 2016 edition of the award.

We present an interpretation of a version of dependent type theory where a type is interpreted by a Kan semisimplicial set. This interprets only a weak notion of conversion similar to the one used in the first published version of Martin-Löf type theory. Each truncated version of this model can be carried out internally in dependent type theory, and we have formalized the first truncated level, which is enough to represent isomorphisms of algebraic structure as equality.

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 article, we report on the formal development of certified programs to compute persistent Betti numbers , an instrumental tool of persistent homology, using the C oq proof assistant together with the SSR eflect 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.

The goal of this note is to show the uniform continuity of definable functional in intuitionistic type theory as an application of forcing with dependent type theory.

The decidability of equality is proved for Martin-Löf type theory with a universe á la Russell and typed beta-eta- equality judgements. A corollary of this result is that the constructor for dependent function types is injective, a property which is crucial for establishing the correctness of the type-checking algorithm. The decision procedure uses normalization by evaluation, an algorithm which first interprets terms in a domain with untyped semantic elements and then extracts normal forms. The correctness of this algorithm is established using a PER-model and a logical relation between syntax and semantics.

Ulrich Berger presented a powerful proof of strong normalisation using domains, in particular it simplifies significantly Tait's proof of strong normalisation of Spector's bar recursion. The main contribution of this paper is to show that, using ideas from intersection types and Martin-Lof's domain interpretation of type theory one can in turn simplify further U. Berger's argument. We build a domain model for an untyped programming language where U. Berger has an interpretation only for typed terms or alternatively has an interpretation for untyped terms but need an extra condition to deduce strong normalisation. As a main application, we show that Martin-L\"{o}f dependent type theory extended with a program for Spector double negation shift.

U. Bergel; [ I I ] signijicantly simplijied Tait's normalisation proof for bar recursion [27], see also [9], replacing Tait's introduction of injinite terms by the construction of a domain having the property that a term is strongly normalizing if its semantics is \ne. The goal of this paper is to show that, using ideas from the theory of intersection types [2, 6, 7, 211 and Martin-Liif's domain interpretation of type theory [18], we can in turn simplify U. Berger's argument in the construction of such a domain model. We think that our domain model can be used to give modular proofs of strong normalization for various type theory. As an example, we show in some details how it can be used to prove strong normalization for Martin-Liif dependent type theory extended with bar recursion, and with some form ofproof-irrelevance.

Pure Type Systems (PTS) come in two flavours: domain-free systems with untyped $\lambda$ -abstractions (i.e. of the form $\lambda{x}.{M}$ ); and domain-free systems with typed $\lambda$ -abstractions (i.e. of the form $\lambda{x}{A}{M}$ ). Both flavours of systems are related by an erasure function $\er{.}$ that removes types from $\lambda$ -abstractions. Preservation of Equational Theory , which states the equational theories of both systems coincide through the erasure function, is a property of functional and normalizing PTSs. In this paper we establish that Preservation of Equational Theory fails for some non-normalizing PTSs, including the PTS with $\ast:\ast$. The gist of our argument is to exhibit a typable expression $Y_H$ whose erasure $\er{Y}$ is a fixpoint combinator, but which is not a fixpoint combinator itself.

Recent work in constructive mathematics shows that Hilbert's program works for a large part of abstract algebra. Using in an essential way the ideas contained in the classical arguments, we can transform most of the highly abstract proofs of ‘concrete’ statements into elementary proofs. Surprisingly, the arguments we produce are not only elementary but also mathematically clearer, and not necessarily longer. We present an example where the simplification was significant enough to suggest an improved version of a classical theorem. For this we use a general method to transform some logically complex first-order formulae into a geometrical form, which may be interesting in itself.

The completeness proof for first-order logic by Rasiowa and Sikorski [13] is a simplification of Henkin's proof [7] in that it avoids the addition of infinitely many new individual constants. Instead they show that each consistent set of formulae can be extended to a maximally consistent set, satisfying the following existence property: if it contains (∃x)ϕit also contains some substitutionϕ(y/x) of a variableyforx. In Feferman's review [5] of [13], an improvement, due to Tarski, is given by which the proof gets a simple algebraic form. Sambin [16] used the same method in the setting of formal topology [15], thereby obtaining a constructive completeness proof. This proof is elementary and can be seen as a constructive and predicative version of the one in Feferman's review. It is a typical, and simple, example where the use of formal topology gives constructive sense to the existence of a generic object, satisfying some forcing conditions; in this case an ultrafilter satisfying the existence property. In order to get a formal topology on the set of first-order formulae, Sambin used the Dedekind-MacNeille completion to define a covering relation ⊲DM. This method, by which an arbitrary poset can be extended to a complete poset, was introduced by MacNeille [9] and is a generalization of the construction of real numbers from rationals by Dedekind cuts. It is also possible to define an inductive cover, ⊲I, on the set of formulae, which can also be used to give canonical models, see Coquand and Smith [3].

Abstract We present a possible computational content of the negative translation of classical analysis with the Axiom of (countable) Choice. Interestingly, this interpretation uses a refinement of the realizability semantics of the absurdity proposition, which is not interpreted as the empty type here. We also show how to compute witnesses from proofs in classical analysis of ∃-statements and how to extract algorithms from proofs of ∀∃-statements. Our interpretation seems computationally more direct than the one based on Gödel's Dialectica interpretation.

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.

The traditional notions of strong and weak normalization refer to properties of a binary reduction relation. In this paper we explore an alternative approach to normalization, in which we bypass the reduction relation and instead focus on the normalization function, that is, the function that maps a term to its normal form. We work in an intuitionistic metalanguage, and characterize a normalization function as an algorithm that picks a canonical representative from the equivalence class of convertible terms. This means that we also get a decision algorithm for convertibility.Such a normalization function can be constructed by building an appropriate model and a function quote, which inverts the interpretation function. The normalization function is then obtained by composing the quote function with the interpretation function. We also discuss how to get a simple proof of the property that constructors are one-to-one, which is usually obtained as a corollary of Church–Rosser and normalization in the traditional sense.We illustrate this approach by showing how a glueing model (closely related to the glueing construction used in category theory) gives rise to a normalization algorithm for a combinatory formulation of Gödel System T. We then show how the method extends in a straightforward way when we add cartesian products and disjoint unions (full intuitionistic propositional logic under a Curry–Howard interpretation) and transfinite inductive types such as the Brouwer ordinals.

If it is difficult to give the exact significance of consistency proofs from a classical point of view, in particular the proofs of Gentzen [2, 6], and Novikoff [14], the motivations of these proofs are quite clear intuitionistically. Their significance is then less to give a mere consistency proof than to present an intuitionistic explanation of the notion of classical truth. Gentzen for instance summarizes his proof as follows [6]: “Thus propositions of actualist mathematics seem to have a certain utility, but no sense. The major part of my consistency proof, however, consists precisely in ascribing a finitist sense to actualist propositions.” From this point of view, the main part of both Gentzen's and Novikoff's arguments can be stated as establishing that modus ponens is valid w.r.t. this interpretation ascribing a “finitist sense” to classical propositions. In this paper, we reformulate Gentzen's and Novikoff's “finitist sense” of an arithmetic proposition as a winning strategy for a game associated to it. (To see a proof as a winning strategy has been considered by Lorenzen [10] for intuitionistic logic.) In the light of concurrency theory [7], it is tempting to consider a strategy as an interactive program (which represents thus the “finitist sense” of an arithmetic proposition). We shall show that the validity of modus ponens then gets a quite natural formulation, showing that “internal chatters” between two programs end eventually. We first present Novikoff's notion of regular formulae, that can be seen as an intuitionistic truth definition for classical infinitary propositional calculus. We use this in order to motivate the second part, which presents a game-theoretic interpretation of the notion of regular formulae, and a proof of the admissibility of modus ponens which is based on this interpretation.

Abstract We present here a generalization of A-translation to a class of pure type systems. We apply this translation to give a direct proof of the existence of a looping combinator in a large class of inconsistent type systems, a class which includes type systems with a type of all types. This is the first non-automated solution to this problem.

Tychonoff's theorem states that a product of compact spaces is compact. In [3], P. Johnstone presents a proof of Tychonoff's theorem in a “localic” framework. The surprise is that the point-free formulation of Tychonoff's theorem is provable without the axiom of choice, whereas in the usual formulation it is equivalent to the axiom of choice (see Kelley [5]). The proof given in [3], however, is classical and seems to use the replacement axiom of Zermelo-Fraenkel. The aim of this paper is to present what we believe to be a more direct proof, which is intuitionistic and can be proved using as primitive only the notion of inductive definition, as it is for instance presented in Martin-Löf [6]. One main point of the paper is to show that the theory of locales can be developed rather naturally in the framework of inductive definitions. We think that our arguments can be presented in the constructive set theory of Aczel [2]. The paper is organized as follows. In §1 we show the argument in the case of a product of two spaces. This proof has a direct generalisation to the case of a product over a set with a decidable equality. §1. Product of two spaces. We first recall a possible definition of a point-free space (see Johnstone [3] or Vickers [10]). It is a poset (X, ≤), together with a meet operation ab, written multiplicatively, and, for each a ∈ X, a set Cov(a) of subsets of {x ∈ X ∣ x ≤ a}. We ask that if M ∈ Cov(a) and b ≤ a, then {bs ∈ s ∈ M} ∈ Cov(b). This property of Cov will be called the axiom of covering. The elements of Cov(u) are called basic covers of u ∈ X.

We present a method for providing semantic interpretations for languages with a type system featuring inheritance polymorphism. Our approach is illustrated on an extension of the language Fun of Cardelli and Wegner, which we interpret via a translation into an extended polymorphic lambda calculus. Our goal is to interpret inheritances in Fun via coercion functions which are definable in the target of the translation. Existing techniques in the theory of semantic domains can be then used to interpret the extended polymorphic lambda calculus, thus providing many models for the original language. This technique makes it possible to model a rich type discipline which includes parametric polymorphism and recursive types as well as inheritance. A central difficulty in providing interpretations for explicit type disciplines featuring inheritance in the sense discussed in this paper arises from the fact that programs can type-check in more than one way. Since interpretations follow the type-checking derivations, coherence theorems are required: that is, one must prove that the meaning of a program does not depend on the way it was type-checked. Proofs of such theorems for our proposed interpretation are the basic technical results of this paper. Interestingly, proving coherence in the presence of recursive types, variants, and abstract types forced us to reexamine fundamental equational properties that arise in proof theory (in the form of commutative reductions) and domain theory (in the form of strict vs. non-strict functions).

A method is presented for providing semantic interpretations for languages which feature inheritance in the framework of statically checked, rich type disciplines. The approach is illustrated by an extension of the language Fun of L. Cardelli and P. Wegner (1985), which is interpreted via a translation into an extended polymorphic lambda calculus. The approach interprets inheritances in Fun as coercion functions already definable in the target of the translation. Existing techniques in the theory of semantic domains can then be used to interpret the extended polymorphic lambda calculus, thus providing many models for the original language. The method allows the simultaneous modeling of parametric polymorphism, recursive types, and inheritance, which has been regarded as problematic because of the seemingly contradictory characteristics of inheritance and type recursion on higher types. The main difficulty in providing interpretations for explicit type disciplines featuring inheritance is identified. Since interpretations follow the type-checking derivations, coherence theorems are required, and the authors prove them for their semantic method.>

A categorical generalization of the notion of domains, which is stable by (suitable) exponentiation is presented. The goal was originally to generalize J.Y. Girard's (1986) model of polymorphism to F omega . If this notion is specialized to the poset case, a novel Cartesian closed category of domains is obtained.>

We present a general method for constructing extensional models for the Girard-Reynolds polymorphic lambda calculus—the polymorphic extensional collapse. The method yields models that satisfy additional, computationally motivated constraints like having only two polymorphic booleans and having only the numerals as polymorphic integers. Moreover, the method can be used to show that any simply typed lambda model can be fully and faithfully embedded into a model of the polymorphic lambda calculus.