On Small Types in Univalent Foundations
From MaRDI portal
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 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.
Cites work
- scientific article; zbMATH DE number 4152376 (Why is no real title available?)
- scientific article; zbMATH DE number 4002093 (Why is no real title available?)
- scientific article; zbMATH DE number 7561492 (Why is no real title available?)
- A lattice-theoretical fixpoint theorem and its applications
- A univalent formalization of the \(p\)-adic numbers
- ABSTRACT INDUCTIVE AND CO-INDUCTIVE DEFINITIONS
- An experimental library of formalized mathematics based on the univalent foundations
- Apartness and uniformity. A constructive development.
- Connecting constructive notions of ordinals in homotopy type theory
- Continuous Lattices and Domains
- Cubical type theory: a constructive interpretation of the univalence axiom
- Embedding locales and formal topologies into positive topologies
- Formal Baire space in constructive set theory
- Homotopy type theory. Univalent foundations of mathematics
- Idempotents in intensional type theory
- Inductively generated formal topologies.
- Joins in the frame of nuclei
- Mathematical Applications of Category Theory
- Notions of anonymous existence in Martin-Löf type theory
- On Tarski’s fixed point theorem
- On some peculiar aspects of the constructive theory of point-free spaces
- On the existence of Stone-Čech compactification
- Partial elements and recursion via dominances in univalent type theory
- Positivity relations on a locale
- Predicative Aspects of Order Theory in Univalent Foundations
- Sets in homotopy type theory
- Some points in formal topology.
- The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
- The real projective spaces in homotopy type theory
- The simplicial model of univalent foundations (after Voevodsky)
- Univalence for inverse diagrams and homotopy canonicity
- Zorn's lemma and complete Boolean algebras in intuitionistic type theories
Cited in
(2)
This page was built for publication: On Small Types in Univalent Foundations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6135756)
