On Small Types in Univalent Foundations
From MaRDI portal
Publication:6135756
DOI10.46298/lmcs-19(2:8)2023arXiv2111.00482OpenAlexW4381480147MaRDI QIDQ6135756
Tom J. de Jong, Martín Hötzel Escardó
Publication date: 26 August 2023
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2111.00482
constructive mathematicshomotopy type theoryorder theorycomplete posetsordinalspredicative mathematicsunivalent foundationspropositional resizingHoTT/UFpropositional truncationsset quotientsset replacementtype universes
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Positivity relations on a locale
- Joins in the frame of nuclei
- Inductively generated formal topologies.
- Some points in formal topology.
- Embedding locales and formal topologies into positive topologies
- The simplicial model of univalent foundations (after Voevodsky)
- A lattice-theoretical fixpoint theorem and its applications
- On Tarski’s fixed point theorem
- Idempotents in intensional type theory
- On the existence of Stone-Čech compactification
- Apartness and Uniformity
- Mathematical Applications of Category Theory
- On some peculiar aspects of the constructive theory of point-free spaces
- Zorn's lemma and complete Boolean algebras in intuitionistic type theories
- ABSTRACT INDUCTIVE AND CO-INDUCTIVE DEFINITIONS
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- Continuous Lattices and Domains
- Partial Elements and Recursion via Dominances in Univalent Type Theory.
- The real projective spaces in homotopy type theory
- The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
- Homotopy Type Theory: Univalent Foundations of Mathematics
- A univalent formalization of the p-adic numbers
- Sets in homotopy type theory
- Univalence for inverse diagrams and homotopy canonicity
- An experimental library of formalized Mathematics based on the univalent foundations
- Predicative Aspects of Order Theory in Univalent Foundations
