-
Internal Effectful Forcing in System T
Authors:
Martin H. Escardo,
Bruno da Rocha Paiva,
Vincent Rahli,
Ayberk Tosun
Abstract:
The effectful forcing technique allows one to show that the denotation of a closed System T term of type $(ι\to ι) \to ι$ in the set-theoretical model is a continuous function $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$. For this purpose, an alternative dialogue-tree semantics is defined and related to the set-theoretical semantics by a logical relation. In this paper, we apply effectful forcing…
▽ More
The effectful forcing technique allows one to show that the denotation of a closed System T term of type $(ι\to ι) \to ι$ in the set-theoretical model is a continuous function $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$. For this purpose, an alternative dialogue-tree semantics is defined and related to the set-theoretical semantics by a logical relation. In this paper, we apply effectful forcing to show that the dialogue tree of a System T term is itself System T-definable, using the Church encoding of trees.
△ Less
Submitted 16 May, 2025;
originally announced May 2025.
-
Euclidean interval objects in categories with finite products
Authors:
Martin Escardo,
Alex Simpson
Abstract:
Based on the intuitive notion of convexity, we formulate a universal property defining interval objects in a category with finite products. Interval objects are structures corresponding to closed intervals of the real line, but their definition does not assume a pre-existing notion of real number. The universal property characterises such structures up to isomorphism, supports the definition of fu…
▽ More
Based on the intuitive notion of convexity, we formulate a universal property defining interval objects in a category with finite products. Interval objects are structures corresponding to closed intervals of the real line, but their definition does not assume a pre-existing notion of real number. The universal property characterises such structures up to isomorphism, supports the definition of functions between intervals, and provides a means of verifying identities between functions. In the category of sets, the universal property characterises closed intervals of real numbers with nonempty interior. In the the category of topological spaces, we obtain intervals with the Euclidean topology. We also prove that every elementary topos with natural numbers object contains an interval object; furthermore, we characterise interval objects as intervals of real numbers in the Cauchy completion of the rational numbers within the Dedekind reals.
△ Less
Submitted 30 April, 2025;
originally announced April 2025.
-
Domain theory in univalent foundations II: Continuous and algebraic domains
Authors:
Tom de Jong,
Martín Hötzel Escardó
Abstract:
We develop the theory of continuous and algebraic domains in constructive and predicative univalent foundations, building upon our earlier work on basic domain theory in this setting. That we work predicatively means that we do not assume Voevodsky's propositional resizing axioms. Our work is constructive in the sense that we do not rely on excluded middle or the axiom of (countable) choice. To de…
▽ More
We develop the theory of continuous and algebraic domains in constructive and predicative univalent foundations, building upon our earlier work on basic domain theory in this setting. That we work predicatively means that we do not assume Voevodsky's propositional resizing axioms. Our work is constructive in the sense that we do not rely on excluded middle or the axiom of (countable) choice. To deal with size issues and give a predicatively suitable definition of continuity of a dcpo, we follow Johnstone and Joyal's work on continuous categories. Adhering to the univalent perspective, we explicitly distinguish between data and property. To ensure that being continuous is a property of a dcpo, we turn to the propositional truncation, although we explain that some care is needed to avoid needing the axiom of choice. We also adapt the notion of a domain-theoretic basis to the predicative setting by imposing suitable smallness conditions, analogous to the categorical concept of an accessible category. All our running examples of continuous dcpos are then actually examples of dcpos with small bases which we show to be well behaved predicatively. In particular, such dcpos are exactly those presented by small ideals. As an application of the theory, we show that Scott's $D_\infty$ model of the untyped $λ$-calculus is an example of an algebraic dcpo with a small basis. Our work is formalised in the Agda proof assistant and its ability to infer universe levels has been invaluable for our purposes.
△ Less
Submitted 18 July, 2024; v1 submitted 9 July, 2024;
originally announced July 2024.
-
Kreisel's counter-example to full abstraction of the set-theoretical model of Goedel's system T
Authors:
Martin Escardo
Abstract:
The set-theoretical model of Goedel's system T is not fully abstract. We also briefly discuss fully abstract models of system T.
The set-theoretical model of Goedel's system T is not fully abstract. We also briefly discuss fully abstract models of system T.
△ Less
Submitted 16 March, 2023;
originally announced March 2023.
-
Patch Locale of a Spectral Locale in Univalent Type Theory
Authors:
Ayberk Tosun,
Martín Hötzel Escardó
Abstract:
Stone locales together with continuous maps form a coreflective subcategory of spectral locales and perfect maps. A proof in the internal language of an elementary topos was previously given by the second-named author. This proof can be easily translated to univalent type theory using resizing axioms. In this work, we show how to achieve such a translation without resizing axioms, by working with…
▽ More
Stone locales together with continuous maps form a coreflective subcategory of spectral locales and perfect maps. A proof in the internal language of an elementary topos was previously given by the second-named author. This proof can be easily translated to univalent type theory using resizing axioms. In this work, we show how to achieve such a translation without resizing axioms, by working with large, locally small, and small complete frames with small bases. This turns out to be nontrivial and involves predicative reformulations of several fundamental concepts of locale theory.
△ Less
Submitted 20 February, 2023; v1 submitted 11 January, 2023;
originally announced January 2023.
-
Higher-order Games with Dependent Types
Authors:
Martín Escardó,
Paulo Oliva
Abstract:
In previous work on higher-order games, we accounted for finite games of unbounded length by working with continuous outcome functions, which carry implicit game trees. In this work we make such trees explicit. We use concepts from dependent type theory to capture history-dependent games, where the set of available moves at a given position in the game depends on the moves played up to that point.…
▽ More
In previous work on higher-order games, we accounted for finite games of unbounded length by working with continuous outcome functions, which carry implicit game trees. In this work we make such trees explicit. We use concepts from dependent type theory to capture history-dependent games, where the set of available moves at a given position in the game depends on the moves played up to that point. In particular, games are modelled by a W-type, which is essentially the same type used by Aczel to model constructive Zermelo-Frankel set theory (CZF). We have also implemented all our definitions, constructions, results and proofs in the dependently-typed programming language Agda, which, in particular, allows us to run concrete examples of computations of optimal strategies, that is, strategies in subgame perfect equilibrium.
△ Less
Submitted 7 July, 2023; v1 submitted 15 December, 2022;
originally announced December 2022.
-
On Small Types in Univalent Foundations
Authors:
Tom de Jong,
Martín Hötzel Escardó
Abstract:
We investigate predicative aspects of constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's propositional resizing axioms or excluded middle. Our work complements existing work on predicative mathematics by exploring what cannot be done predicatively in univalent foundations. Our first main result is that nontrivial (directed or…
▽ More
We investigate predicative aspects of constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's propositional resizing axioms or excluded middle. Our work complements existing work on predicative mathematics by exploring what cannot be done predicatively in univalent foundations. Our first main result is that nontrivial (directed or bounded) complete posets are necessarily large. That is, if such a nontrivial poset is small, then weak propositional resizing holds. It is possible to derive full propositional resizing if we strengthen nontriviality to positivity. The distinction between nontriviality and positivity is analogous to the distinction between nonemptiness and inhabitedness. Moreover, we prove that locally small, nontrivial (directed or bounded) complete posets necessarily lack decidable equality. We prove our results for a general class of posets, which includes e.g. directed complete posets, bounded complete posets, sup-lattices and frames. Secondly, the fact that these nontrivial posets are necessarily large has the important consequence that Tarski's theorem (and similar results) cannot be applied in nontrivial instances. Furthermore, we explain that generalizations of Tarski's theorem that allow for large structures are provably false by showing that the ordinal of ordinals in a univalent universe has small suprema in the presence of set quotients. The latter also leads us to investigate the inter-definability and interaction of type universes of propositional truncations and set quotients, as well as a set replacement principle. Thirdly, we clarify, in our predicative setting, the relation between the traditional definition of sup-lattice that requires suprema for all subsets and our definition that asks for suprema of all small families.
△ Less
Submitted 3 May, 2023; v1 submitted 31 October, 2021;
originally announced November 2021.
-
Predicative Aspects of Order Theory in Univalent Foundations
Authors:
Tom de Jong,
Martín Hötzel Escardó
Abstract:
We investigate predicative aspects of order theory in constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's propositional resizing axioms or excluded middle. Our work complements existing work on predicative mathematics by exploring what cannot be done predicatively in univalent foundations. Our first main result is that nontriv…
▽ More
We investigate predicative aspects of order theory in constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's propositional resizing axioms or excluded middle. Our work complements existing work on predicative mathematics by exploring what cannot be done predicatively in univalent foundations. Our first main result is that nontrivial (directed or bounded) complete posets are necessarily large. That is, if such a nontrivial poset is small, then weak propositional resizing holds. It is possible to derive full propositional resizing if we strengthen nontriviality to positivity. The distinction between nontriviality and positivity is analogous to the distinction between nonemptiness and inhabitedness. We prove our results for a general class of posets, which includes directed complete posets, bounded complete posets and sup-lattices, using a technical notion of a $δ_{\mathcal V}$-complete poset. We also show that nontrivial locally small $δ_{\mathcal V}$-complete posets necessarily lack decidable equality. Specifically, we derive weak excluded middle from assuming a nontrivial locally small $δ_{\mathcal V}$-complete poset with decidable equality. Moreover, if we assume positivity instead of nontriviality, then we can derive full excluded middle. Secondly, we show that each of Zorn's lemma, Tarski's greatest fixed point theorem and Pataraia's lemma implies propositional resizing. Hence, these principles are inherently impredicative and a predicative development of order theory must therefore do without them. Finally, we clarify, in our predicative setting, the relation between the traditional definition of sup-lattice that requires suprema for all subsets and our definition that asks for suprema of all small families.
△ Less
Submitted 21 April, 2021; v1 submitted 17 February, 2021;
originally announced February 2021.
-
A Note on Generalized Algebraic Theories and Categories with Families
Authors:
Marc Bezem,
Thierry Coquand,
Peter Dybjer,
Martín Escardó
Abstract:
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 n…
▽ 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. 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.
△ Less
Submitted 16 March, 2021; v1 submitted 15 December, 2020;
originally announced December 2020.
-
Domain Theory in Constructive and Predicative Univalent Foundations
Authors:
Tom de Jong,
Martín Hötzel Escardó
Abstract:
We develop domain theory in constructive univalent foundations without Voevodsky's resizing axioms. In previous work in this direction, we constructed the Scott model of PCF and proved its computational adequacy, based on directed complete posets (dcpos). Here we further consider algebraic and continuous dcpos, and construct Scott's $D_\infty$ model of the untyped $λ$-calculus. A common approach t…
▽ More
We develop domain theory in constructive univalent foundations without Voevodsky's resizing axioms. In previous work in this direction, we constructed the Scott model of PCF and proved its computational adequacy, based on directed complete posets (dcpos). Here we further consider algebraic and continuous dcpos, and construct Scott's $D_\infty$ model of the untyped $λ$-calculus. A common approach to deal with size issues in a predicative foundation is to work with information systems or abstract bases or formal topologies rather than dcpos, and approximable relations rather than Scott continuous functions. Here we instead accept that dcpos may be large and work with type universes to account for this. For instance, in the Scott model of PCF, the dcpos have carriers in the second universe $\mathcal{U}_1$ and suprema of directed families with indexing type in the first universe $\mathcal{U}_0$. Seeing a poset as a category in the usual way, we can say that these dcpos are large, but locally small, and have small filtered colimits. In the case of algebraic dcpos, in order to deal with size issues, we proceed mimicking the definition of accessible category. With such a definition, our construction of Scott's $D_\infty$ again gives a large, locally small, algebraic dcpo with small directed suprema.
△ Less
Submitted 15 June, 2022; v1 submitted 4 August, 2020;
originally announced August 2020.
-
The Cantor-Schröder-Bernstein Theorem for $\infty$-groupoids
Authors:
Martín Hötzel Escardó
Abstract:
We show that the Cantor-Schröder-Bernstein Theorem for homotopy types, or $\infty$-groupoids holds in the following form: For any two types, if each one is embedded into the other, then they are equivalent. The argument is developed in the language of homotopy type theory, or Voevodsky's univalent foundations (HoTT/UF), and requires classical logic. It follows that the theorem holds in any boolean…
▽ More
We show that the Cantor-Schröder-Bernstein Theorem for homotopy types, or $\infty$-groupoids holds in the following form: For any two types, if each one is embedded into the other, then they are equivalent. The argument is developed in the language of homotopy type theory, or Voevodsky's univalent foundations (HoTT/UF), and requires classical logic. It follows that the theorem holds in any boolean $\infty$-topos.
△ Less
Submitted 26 August, 2020; v1 submitted 13 February, 2020;
originally announced February 2020.
-
Intersections of compactly many open sets are open
Authors:
Martín Hötzel Escardó
Abstract:
By definition, the intersection of finitely many open sets of any topological space is open. Nachbin observed that, more generally, the intersection of compactly many open sets is open. Moreover, Nachbin applied this to obtain elegant proofs of various facts concerning compact sets in topology and elsewhere. A simple calculation shows that Nachbin's observation amounts to the well known fact that…
▽ More
By definition, the intersection of finitely many open sets of any topological space is open. Nachbin observed that, more generally, the intersection of compactly many open sets is open. Moreover, Nachbin applied this to obtain elegant proofs of various facts concerning compact sets in topology and elsewhere. A simple calculation shows that Nachbin's observation amounts to the well known fact that if a space $X$ is compact, then the projection map $Z \times X \to Z$ is closed for every space $Z$. It is also well known that the converse holds: if a space $X$ has the property that the projection $Z \times X \to Z$ is closed for every space $Z$, then $X$ is compact. We reformulate this as a converse of Nachbin's observation, and apply this to obtain further elegant proofs of (old and new) theorems concerning compact sets. We also provide a new proof of (a reformulation of) the fact that a space $X$ is compact if and only if the projection map $Z \times X \to Z$ is closed for every space $Z$. This is generalized in various ways, to obtain new results about spaces of continuous functions, proper maps, relative compactness, and compactly generated spaces. In particular, we give an intrinsic description of the binary product in the category of compactly generated spaces in terms of the Scott topology of the lattice of open sets.
△ Less
Submitted 16 January, 2020;
originally announced January 2020.
-
Introduction to Univalent Foundations of Mathematics with Agda
Authors:
Martín Hötzel Escardó
Abstract:
We introduce Voevodsky's univalent foundations and univalent mathematics, and explain how to develop them with the computer system Agda, which is based on Martin-Löf type theory. Agda allows us to write mathematical definitions, constructions, theorems and proofs, for example in number theory, analysis, group theory, topology, category theory or programming language theory, checking them for logic…
▽ More
We introduce Voevodsky's univalent foundations and univalent mathematics, and explain how to develop them with the computer system Agda, which is based on Martin-Löf type theory. Agda allows us to write mathematical definitions, constructions, theorems and proofs, for example in number theory, analysis, group theory, topology, category theory or programming language theory, checking them for logical and mathematical correctness.
Agda is a constructive mathematical system by default, which amounts to saying that it can also be considered as a programming language for manipulating mathematical objects. But we can assume the axiom of choice or the principle of excluded middle for pieces of mathematics that require them, at the cost of losing the implicit programming-language character of the system. For a fully constructive development of univalent mathematics in Agda, we would need to use its new cubical flavour, and we hope these notes provide a base for researchers interested in learning cubical type theory and cubical Agda as the next step.
Compared to most expositions of the subject, we work with explicit universe levels.
△ Less
Submitted 2 September, 2022; v1 submitted 1 November, 2019;
originally announced November 2019.
-
Injective types in univalent mathematics
Authors:
Martín Hötzel Escardó
Abstract:
We investigate the injective types and the algebraically injective types in univalent mathematics, both in the absence and in the presence of propositional resizing. Injectivity is defined by the surjectivity of the restriction map along any embedding, and algebraic injectivity is defined by a given section of the restriction map along any embedding. Under propositional resizing axioms, the main r…
▽ More
We investigate the injective types and the algebraically injective types in univalent mathematics, both in the absence and in the presence of propositional resizing. Injectivity is defined by the surjectivity of the restriction map along any embedding, and algebraic injectivity is defined by a given section of the restriction map along any embedding. Under propositional resizing axioms, the main results are easy to state: (1) Injectivity is equivalent to the propositional truncation of algebraic injectivity. (2) The algebraically injective types are precisely the retracts of exponential powers of universes. (2a) The algebraically injective sets are precisely the retracts of powersets. (2b) The algebraically injective $(n+1)$-types are precisely the retracts of exponential powers of universes of $n$-types. (3) The algebraically injective types are also precisely the retracts of algebras of the partial-map classifier. From (2) it follows that any universe is embedded as a retract of any larger universe. In the absence of propositional resizing, we have similar results which have subtler statements that need to keep track of universe levels rather explicitly, and are applied to get the results that require resizing.
△ Less
Submitted 9 March, 2020; v1 submitted 4 March, 2019;
originally announced March 2019.
-
A self-contained, brief and complete formulation of Voevodsky's Univalence Axiom
Authors:
Martín Hötzel Escardó
Abstract:
In introductions to the subject for a general audience of mathematicians or logicians, the univalence axiom is typically explained by handwaving. This gives rise to several misconceptions, which cannot be properly addressed in the absence of a precise definition. In this short set of notes we give a complete formulation of the univalence axiom from scratch. The underlying idea of these notes is th…
▽ More
In introductions to the subject for a general audience of mathematicians or logicians, the univalence axiom is typically explained by handwaving. This gives rise to several misconceptions, which cannot be properly addressed in the absence of a precise definition. In this short set of notes we give a complete formulation of the univalence axiom from scratch. The underlying idea of these notes is that they should be as concise as possible (and not more). They are not meant to be an Encyclopedia of Univalence.
△ Less
Submitted 16 October, 2018; v1 submitted 6 March, 2018;
originally announced March 2018.
-
Parametricity, automorphisms of the universe, and excluded middle
Authors:
Auke Bart Booij,
Martín Hötzel Escardó,
Peter LeFanu Lumsdaine,
Michael Shulman
Abstract:
It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific instances of non-parametricity. We also address the interaction between classical axioms and the existence of automorphisms of a type universe. We work over intensional Martin-Löf dependent type theory, and in…
▽ More
It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific instances of non-parametricity. We also address the interaction between classical axioms and the existence of automorphisms of a type universe. We work over intensional Martin-Löf dependent type theory, and in some results assume further principles including function extensionality, propositional extensionality, propositional truncation, and the univalence axiom.
△ Less
Submitted 27 June, 2017; v1 submitted 19 January, 2017;
originally announced January 2017.
-
The Herbrand Functional Interpretation of the Double Negation Shift
Authors:
Martin Escardo,
Paulo Oliva
Abstract:
This paper considers a generalisation of selection functions over an arbitrary strong monad $T$, as functionals of type $J^T_R X = (X \to R) \to T X$. It is assumed throughout that $R$ is a $T$-algebra. We show that $J^T_R$ is also a strong monad, and that it embeds into the continuation monad $K_R X = (X \to R) \to R$. We use this to derive that the explicitly controlled product of $T$-selection…
▽ More
This paper considers a generalisation of selection functions over an arbitrary strong monad $T$, as functionals of type $J^T_R X = (X \to R) \to T X$. It is assumed throughout that $R$ is a $T$-algebra. We show that $J^T_R$ is also a strong monad, and that it embeds into the continuation monad $K_R X = (X \to R) \to R$. We use this to derive that the explicitly controlled product of $T$-selection functions is definable from the explicitly controlled product of quantifiers, and hence from Spector's bar recursion. We then prove several properties of this product in the special case when $T$ is the finite power set monad ${\mathcal P}(\cdot)$. These are used to show that when $T X = {\mathcal P}(X)$ the explicitly controlled product of $T$-selection functions calculates a witness to the Herbrand functional interpretation of the double negation shift.
△ Less
Submitted 19 October, 2015; v1 submitted 16 October, 2014;
originally announced October 2014.
-
Bar Recursion and Products of Selection Functions
Authors:
Martin Escardo,
Paulo Oliva
Abstract:
We show how two iterated products of selection functions can both be used in conjunction with system T to interpret, via the dialectica interpretation and modified realizability, full classical analysis. We also show that one iterated product is equivalent over system T to Spector's bar recursion, whereas the other is T-equivalent to modified bar recursion. Modified bar recursion itself is shown t…
▽ More
We show how two iterated products of selection functions can both be used in conjunction with system T to interpret, via the dialectica interpretation and modified realizability, full classical analysis. We also show that one iterated product is equivalent over system T to Spector's bar recursion, whereas the other is T-equivalent to modified bar recursion. Modified bar recursion itself is shown to arise directly from the iteration of a different binary product of "skewed" selection functions. Iterations of the dependent binary products are also considered but in all cases are shown to be T-equivalent to the iteration of the simple products.
△ Less
Submitted 14 August, 2014; v1 submitted 25 July, 2014;
originally announced July 2014.
