arXiv subjects

Martín Hötzel Escardó

Publications and source records attributed to Martín Hötzel Escardó.

14 recordsLinked to original sources

arXiv2026

Compact totally separated types

Perhaps surprisingly, there are infinite types that can be exhaustively searched mechanically in finite time. We use ideas from topology to build plenty of them, referring to searchable types as compact types, and we use ordinals to measure their logical complexity. We consider two systems of ordinal notations under which a single notation denotes both a discrete ordinal and a compact one, with an embedding of the former into the latter whose image has empty complement. A boolean valued function decides which points in the image of the embedding are isolated and which are topological limit points. The first system consists of the traditional Brouwer codes and the second is an inductive-recursive universe generalizing them. The discrete ordinals so obtained are trichotomous, and the compact ones have the least element property for complemented subsets, but these two desirable properties cannot be fulfilled simultaneously in a constructive setting. The ordinals obtained from Brouwer codes further enjoy a boolean Leibniz principle, which has the notion of total separatedness as its topological counterpart. This extends previous work from G\"odel's system T to intensional Martin-L\"of type theory with univalent universes, and is formalized in Agda in the TypeTopology repository.

math.LO↗

arXiv2026

Examples and counterexamples of injective types

It is known that, in univalent mathematics, type universes, the type of $n$-types in a universe, reflective subuniverses, and the underlying type of any algebra of the lifting monad are all (algebraically) injective. Here, we further show that the type of ordinals, the type of iterative (multi)sets, the underlying type of any pointed directed complete poset, as well as the types of (small) $\infty$-magmas, monoids, and groups are all injective, among other examples. Not all types of mathematical structures are injective in general. For example, the type of inhabited types is injective if and only if all propositions are projective. In contrast, the type of pointed types and the type of non-empty types are always injective. The injectivity of the type of two-element types implies Fourman and \v{S}\v{c}edrov's world's simplest axiom of choice. We also show that there are no nontrivial small injective types unless a weak propositional resizing principle holds. Other counterexamples include the type of booleans, the simple types, the type of Dedekind reals, and the type of conatural numbers, whose injectivity implies weak excluded middle. More generally, any type with an apartness relation and two points apart cannot be injective unless weak excluded middle holds. Finally, we show that injective types have no non-trivial decidable properties, unless weak excluded middle holds, which amounts to a Rice-like theorem for injective types.

math.LO↗

arXiv2024

Continuous and algebraic domains in univalent foundations

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 $\lambda$-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.

cs.LO↗

arXiv2024

The Patch Topology in Univalent Foundations

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 and locally small frames with small bases. This requires predicative reformulations of several fundamental concepts of locale theory in predicative HoTT/UF, which we investigate systematically.

cs.LO↗

arXiv2023

Patch Locale of a Spectral Locale in Univalent Type Theory

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.

cs.LO↗

arXiv2021

On Small Types in Univalent Foundations

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.

cs.LO↗

arXiv2021

Predicative Aspects of Order Theory in Univalent Foundations

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 $\delta_{\mathcal V}$-complete poset. We also show that nontrivial locally small $\delta_{\mathcal V}$-complete posets necessarily lack decidable equality. Specifically, we derive weak excluded middle from assuming a nontrivial locally small $\delta_{\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.

math.LO↗

arXiv2020

Domain Theory in Constructive and Predicative Univalent Foundations

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 $\lambda$-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.

math.LO↗

arXiv2020

The Cantor-Schr\"oder-Bernstein Theorem for $\infty$-groupoids

We show that the Cantor-Schr\"oder-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.

math.AG↗

arXiv2020

Intersections of compactly many open sets are open

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.

math.GN↗

arXiv2019

Introduction to Univalent Foundations of Mathematics with Agda

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\"of 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.

cs.LO↗

arXiv2019

Injective types in univalent mathematics

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.

math.CT↗

arXiv2018

A self-contained, brief and complete formulation of Voevodsky's Univalence Axiom

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.

math.LO↗

arXiv2017

Parametricity, automorphisms of the universe, and excluded middle

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\"of dependent type theory, and in some results assume further principles including function extensionality, propositional extensionality, propositional truncation, and the univalence axiom.

cs.LO↗