references.bib

@online{1000+theorems,
  title         = {1000+ theorems},
  author        = {1000plus},
  url           = {https://1000-plus.github.io/},
  citeas        = {1000+},
}

@online{100theorems,
  title         = {Formalizing 100 Theorems},
  author        = {Freek Wiedijk},
  url           = {https://www.cs.ru.nl/~freek/100/},
}

@misc{AB26,
  title         = {Sheaves as oracle computations},
  author        = {Danel Ahman and Andrej Bauer},
  year          = 2026,
  eprint        = {2602.22135},
  archiveprefix = {arXiv},
  primaryclass  = {math.LO},
}

@article{ABFJ20,
  title         = {A generalized {{Blakers–Massey}} theorem},
  author        = {Anel, Mathieu and Biedermann, Georg and Finster, Eric and Joyal, Andr\'e},
  year          = 2020,
  journal       = {J. Topol.},
  fjournal      = {Journal of Topology},
  volume        = 13,
  number        = 4,
  pages         = {1521--1553},
  doi           = {10.1112/topo.12163},
  issn          = {1753-8416,1753-8424},
  mrclass       = {18N20 (18B25 18N45 55U35)},
  mrnumber      = 4186137,
  mrreviewer    = {Charles Rezk},
}

@article{AKS15,
  title         = {Univalent Categories and the {{Rezk}} Completion},
  author        = {Ahrens, Benedikt and Kapulkin, Krzysztof and Shulman, Michael},
  year          = 2015,
  month         = {06},
  journal       = {Mathematical Structures in Computer Science},
  volume        = 25,
  number        = 5,
  pages         = {1010--1039},
  doi           = {10.1017/S0960129514000486},
  issn          = {0960-1295, 1469-8072},
  eprint        = {1303.0584},
  eprinttype    = {arxiv},
  eprintclass   = {math},
  abstract      = {We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of ‘category’ for which equality and equivalence of categories agree. Such categories satisfy a version of the univalence axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them ‘saturated’ or ‘univalent’ categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.},
  langid        = {english},
}

@article{AL19,
  title         = {Displayed Categories},
  author        = {Ahrens, Benedikt and LeFanu Lumsdaine, Peter},
  year          = 2019,
  month         = {03},
  journal       = {{Logical Methods in Computer Science}},
  volume        = 15,
  doi           = {10.23638/LMCS-15(1:20)2019},
  eprint        = {1705.04296},
  eprinttype    = {arxiv},
  eprintclass   = {math},
  issue         = 1,
  keywords      = {Mathematics - Category Theory ; Mathematics - Logic ; 18A15, 03B15, 03B70 ; F.4.1},
  langid        = {english},
}

@misc{Anel24,
  title         = {The category of $\pi$-finite spaces},
  author        = {Mathieu Anel},
  year          = 2024,
  eprint        = {2107.02082},
  archiveprefix = {arXiv},
  eprintclass   = {math},
  primaryclass  = {math.CT},
}

@article{ANST25,
  title         = {The Univalence Principle},
  author        = {Benedikt Ahrens and Paige Randall North and Michael Shulman and Dimitris Tsementzis},
  year          = 2025,
  journal       = {Mem. Amer. Math. Soc.},
  fjournal      = {Memoirs of the American Mathematical Society},
  volume        = 305,
  number        = 1541,
  pages         = {vii+175},
  doi           = {10.1090/memo/1541},
  isbn          = {978-1-4704-7269-6; 978-1-4704-8043-1},
  issn          = {0065-9266,1947-6221},
  eprint        = {2102.06275},
  archiveprefix = {arXiv},
  primaryclass  = {math.CT},
  mrclass       = {18N45 (03B38 03G30 55U35)},
  mrnumber      = 4853272,
}

@misc{Awodey22,
  title         = {On {{Hofmann–Streicher}} universes},
  author        = {Awodey, Steve},
  year          = 2022,
  month         = may,
  eprint        = {2205.10917},
  archiveprefix = {arXiv},
  primaryclass  = {math.CT},
  keywords      = {Mathematics - Category Theory, Mathematics - Logic},
}

@article{BauerTaylor2009,
  title         = {The {{Dedekind}} Reals in Abstract {{Stone}} Duality},
  author        = {Bauer, Andrej and Taylor, Paul},
  year          = 2009,
  journal       = {Mathematical Structures in Computer Science},
  publisher     = {Cambridge University Press},
  volume        = 19,
  pages         = {757--838},
  doi           = {10.1017/S0960129509007695},
  url           = {PaulTaylor.EU/ASD/dedras/},
  amsclass      = {03F60, 06E15, 18C20, 26E40, 54D45, 65G40},
}

@online{BCDE21,
  title         = {Free groups in {{HoTT/UF}} in Agda},
  author        = {Bezem, Marc and Coquand, Thierry and Dybjer, Peter and Escardó, Martín},
  year          = 2021,
  url           = {https://www.cs.bham.ac.uk/~mhe/TypeTopology/Groups.Free.html},
}

@online{BCFR23,
  title         = {Central {{H-spaces}} and Banded Types},
  author        = {Buchholtz, Ulrik and Christensen, J. Daniel and Flaten, Jarl G. Taxerås and Rijke, Egbert},
  year          = 2023,
  month         = {02},
  date          = {2023-02-27},
  eprint        = {2301.02636},
  eprinttype    = {arxiv},
  eprintclass   = {cs, math},
  abstract      = {We introduce and study central types, which are generalizations of Eilenberg-Mac Lane spaces. A type is central when it is equivalent to the component of the identity among its own self-equivalences. From centrality alone we construct an infinite delooping in terms of a tensor product of banded types, which are the appropriate notion of torsor for a central type. Our constructions are carried out in homotopy type theory, and therefore hold in any $\infty$-topos. Even when interpreted into the $\infty$-topos of spaces, our main results and constructions are new. Along the way, we further develop the theory of H-spaces in homotopy type theory, including their relation to evaluation fibrations and Whitehead products. These considerations let us, for example, rule out the existence of H-space structures on the $2n$-sphere for $n {$>$} 0$. We also give a novel description of the moduli space of H-space structures on an H-space. Using this description, we generalize a formula of Arkowitz-Curjel and Copeland for counting the number of path components of this moduli space. As an application, we deduce that the moduli space of H-space structures on the $3$-sphere is $\Omega^6 \mathbb{S}^3$.},
  pubstate      = {preprint},
  keywords      = {Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Logic},
}

@online{BdJR24,
  title         = {Epimorphisms and {{Acyclic Types}} in {{Univalent Mathematics}}},
  author        = {Buchholtz, Ulrik and de Jong, Tom and Rijke, Egbert},
  year          = 2024,
  month         = {01},
  date          = {2024-01-25},
  eprint        = {2401.14106},
  eprinttype    = {arxiv},
  eprintclass   = {cs, math},
  abstract      = {We characterize the epimorphisms in homotopy type theory (HoTT) as the fiberwise acyclic maps and develop a type-theoretic treatment of acyclic maps and types in the context of synthetic homotopy theory. We present examples and applications in group theory, such as the acyclicity of the Higman group, through the identification of groups with $0$-connected, pointed $1$-types. Many of our results are formalized as part of the agda-unimath library.},
  pubstate      = {preprint},
  keywords      = {Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Category Theory},
}

@misc{BELS17,
  title         = {Parametricity, automorphisms of the universe, and excluded middle},
  author        = {Auke Bart Booij and Martín Hötzel Escardó and Peter LeFanu Lumsdaine and Michael Shulman},
  year          = 2017,
  eprint        = {1701.05617},
  archiveprefix = {arXiv},
  primaryclass  = {cs.LO},
}

@misc{BH19,
  title         = {A constructive Knaster-Tarski proof of the uncountability of the reals},
  author        = {Ingo Blechschmidt and Matthias Hutzler},
  year          = 2019,
  eprint        = {1902.07366},
  archiveprefix = {arXiv},
  primaryclass  = {math.HO},
}

@misc{BH25,
  title         = {The Countable Reals},
  author        = {Andrej Bauer and James E. Hanson},
  year          = 2025,
  eprint        = {2404.01256},
  archiveprefix = {arXiv},
  primaryclass  = {math.LO},
}

@book{BishopFoundations,
  title         = {Foundations of constructive analysis},
  author        = {Bishop, Errett},
  year          = 2012,
  publisher     = {Ishi Press International},
  address       = {New York ; Tokyo},
  isbn          = 9784871877145,
  language      = {eng},
}

@phdthesis{Booij20PhD,
  title         = {Analysis in univalent type theory},
  author        = {Booij, Auke Bart},
  year          = 2020,
  url           = {https://etheses.bham.ac.uk/id/eprint/10411/7/Booij20PhD.pdf},
  school        = {University of Birmingham},
}

@incollection{BR17,
  title         = {The real projective spaces in homotopy type theory},
  author        = {Buchholtz, Ulrik and Rijke, Egbert},
  year          = 2017,
  booktitle     = {2017 32nd {A}nnual {ACM}/{IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS})},
  publisher     = {IEEE, [Piscataway], NJ},
  pages         = 8,
  isbn          = {978-1-5090-3018-7},
  mrclass       = {55U40 (03B15 03G30 18G55)},
  mrnumber      = 3776972,
}

@book{BSCS05,
  title         = {Absztrakt algebrai feladatok},
  author        = {Bálintné Szendrei, Mária and Czédli, Gábor and Szendrei, Ágnes},
  year          = 2005,
  publisher     = {Polygon},
  url           = {https://interkonyv.hu/konyvek/balintne-szendrei-maria-czedli-gabor-szendrei-agnes-absztrakt-algebrai-feladatok/},
  pagetotal     = 523,
  langid        = {hungarian},
}

@book{BV06,
  title         = {Techniques of Constructive Analysis},
  author        = {Bridges, Douglas S. and Vîţă, Luminiţa Simona},
  year          = 2006,
  publisher     = {Springer-Verlag New York},
  isbn          = {978-0-387-33646-6},
  langid        = {english},
}

@inproceedings{BvDR18,
  title         = {Higher {{Groups}} in {{Homotopy Type Theory}}},
  author        = {Buchholtz, Ulrik and van Doorn, Floris and Rijke, Egbert},
  year          = 2018,
  month         = {02},
  date          = {2018-02-12},
  booktitle     = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
  location      = {Oxford, United Kingdom},
  publisher     = {Association for Computing Machinery},
  address       = {New York, NY, USA},
  series        = {LICS '18},
  pages         = {205--214},
  doi           = {10.1145/3209108.3209150},
  isbn          = 9781450355834,
  eprint        = {1802.04315},
  eprinttype    = {arxiv},
  eprintclass   = {cs, math},
  abstract      = {We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-L\"of type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an $n$-type can be delooped $n+2$ times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.},
  numpages      = 10,
}

@article{BW23,
  title         = {Synthetic Fibered $(\infty,1)$-Category Theory},
  author        = {Buchholtz, Ulrik and Weinberger, Jonathan},
  year          = 2023,
  month         = {05},
  journal       = {Higher Structures},
  volume        = 7,
  pages         = {74--165},
  doi           = {10.21136/HS.2023.04},
  eprint        = {2105.01724},
  eprinttype    = {arxiv},
  eprintclass   = {cs, math},
  abstract      = {We study cocartesian fibrations in the setting of the synthetic $(\infty,1)$-category theory developed in the simplicial type theory introduced by Riehl and Shulman. Our development culminates in a Yoneda Lemma for cocartesian fibrations.},
  pubstate      = {preprint},
  keywords      = {03B38 18N60 18N45 18D30 18N55 55U35 18N50 18D40 18D70,Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic},
}

@article{Cantor1890/91,
  title         = {Über eine elementare Frage der Mannigfaltigketislehre},
  author        = {Cantor, Georg},
  year          = {1890/91},
  journal       = {Jahresbericht der Deutschen Mathematiker-Vereinigung},
  volume        = 1,
  pages         = {72--78},
  url           = {http://eudml.org/doc/144383},
  langid        = {german},
}

@article{Cheng07,
  title         = {An ω-Category with All Duals Is an ω-Groupoid},
  author        = {Cheng, Eugenia},
  year          = 2007,
  month         = {08},
  date          = {2007-08-01},
  journal       = {Applied Categorical Structures},
  volume        = 15,
  number        = 4,
  pages         = {439--453},
  doi           = {10.1007/s10485-007-9081-8},
  issn          = {1572-9095},
  abstract      = {We make a definition of ω-precategory which should underlie any definition of weak ω-category. We make a precise definition of pseudo-invertible cells in this setting. We show that in an ω-precategory with all weak duals, every cell is pseudo-invertible. We deduce that in any “sensible” theory of ω-categories, an ω-category with all weak duals is an ω-groupoid. We discuss various examples and open questions involving higher-dimensional tangles and cobordisms.},
  langid        = {english},
}

@unpublished{Cisinski24,
  title         = {Formalization of higher categories},
  author        = {Denis-Charles Cisinski, Bastiaan Cnossen, Kim Nguyen and Tashi Walde},
  year          = 2024,
  month         = {08},
  date          = {2024-08-10},
  url           = {https://drive.google.com/file/d/1lKaq7watGGl3xvjqw9qHjm6SDPFJ2-0o/view},
  note          = {},
  annote        = {},
}

@article{CORS20,
  title         = {Localization in {{Homotopy Type Theory}}},
  author        = {Christensen, J. Daniel and Opie, Morgan and Rijke, Egbert and Scoccola, Luis},
  year          = 2020,
  month         = {02},
  date          = {2020-02-09},
  journal       = {Higher Structures},
  shortjournal  = {High.Struct.},
  volume        = 4,
  number        = 1,
  pages         = {1--32},
  doi           = {10.21136/HS.2020.01},
  issn          = {2209-0606},
  eprint        = {1807.04155},
  eprinttype    = {arxiv},
  eprintclass   = {math},
  url           = {http://articles.math.cas.cz/10.21136/HS.2020.01},
  mrclass       = {18E35 (03B38 18N45)},
  mrnumber      = 4074272,
  mrreviewer    = {J\'{e}r\^{o}me\ Scherer},
  abstract      = {We study localization at a prime in homotopy type theory, using self maps of the circle. Our main result is that for a pointed, simply connected type $X$, the natural map $X \to X_{(p)}$ induces algebraic localizations on all homotopy groups. In order to prove this, we further develop the theory of reflective subuniverses. In particular, we show that for any reflective subuniverse $L$, the subuniverse of $L$-separated types is again a reflective subuniverse, which we call $L'$. Furthermore, we prove results establishing that $L'$ is almost left exact. We next focus on localization with respect to a map, giving results on preservation of coproducts and connectivity. We also study how such localizations interact with other reflective subuniverses and orthogonal factorization systems. As key steps towards proving the main theorem, we show that localization at a prime commutes with taking loop spaces for a pointed, simply connected type, and explicitly describe the localization of an Eilenberg-Mac Lane space $K(G,n)$ with $G$ abelian. We also include a partial converse to the main theorem.},
  keywords      = {55P60 (Primary) 18E35 03B15 (Secondary),Mathematics - Algebraic Topology,Mathematics - Category Theory},
}

@article{CR21,
  title         = {Modal Descent},
  author        = {Cherubini, Felix and Rijke, Egbert},
  year          = 2021,
  month         = {04},
  date          = {2021-04},
  journal       = {Mathematical Structures in Computer Science},
  volume        = 31,
  number        = 4,
  pages         = {363--391},
  doi           = {10.1017/S0960129520000201},
  issn          = {0960-1295, 1469-8072},
  eprint        = {2003.09713},
  eprinttype    = {arxiv},
  eprintclass   = {math},
  abstract      = {Any modality in homotopy type theory gives rise to an orthogonal factorization system of which the left class is stable under pullbacks. We show that there is a second orthogonal factorization system associated with any modality, of which the left class is the class of $○$-equivalences and the right class is the class of $○$-étale maps. This factorization system is called the modal reflective factorization system of a modality, and we give a precise characterization of the orthogonal factorization systems that arise as the modal reflective factorization system of a modality. In the special case of the $n$-truncation, the modal reflective factorization system has a simple description: we show that the $n$-étale maps are the maps that are right orthogonal to the map $\mathbf{1} \to \mathbf{S}^{n+1}$. We use the $○$-étale maps to prove a modal descent theorem: a map with modal fibers into $○X$ is the same thing as a $○$-étale map into a type $X$. We conclude with an application to real-cohesive homotopy type theory and remark how $○$-étale maps relate to the formally étale maps from algebraic geometry.},
  langid        = {english},
  keywords      = {algebraic geometry,cohesive homotopy type theory,factorization systems,Homotopy type theory,modal homotopy type theory},
}

@online{DavidJaz/Cohesion,
  title         = {DavidJaz/Cohesion},
  author        = {David Jaz Meyers},
  url           = {https://github.com/DavidJaz/Cohesion},
  howpublished  = {{{GitHub}} repository},
}

@misc{Diener18,
  title         = {Constructive Reverse Mathematics},
  author        = {Hannes Diener},
  year          = 2018,
  eprint        = {1804.05495},
  archiveprefix = {arXiv},
  primaryclass  = {math.LO},
}

@article{dJE23,
  title         = {{On Small Types in Univalent Foundations}},
  author        = {de Jong, Tom and Escardó, Martín Hötzel},
  year          = 2023,
  month         = {05},
  journal       = {{Logical Methods in Computer Science}},
  volume        = 19,
  doi           = {10.46298/lmcs-19(2:8)2023},
  eprint        = {2111.00482},
  eprinttype    = {arxiv},
  eprintclass   = {cs},
  url           = {https://lmcs.episciences.org/11270},
  issue         = 2,
  keywords      = {Computer Science - Logic in Computer Science ; Mathematics - Logic},
}

@inproceedings{dJKFX23,
  title         = {Set-{{Theoretic}} and {{Type-Theoretic Ordinals Coincide}}},
  author        = {de Jong, Tom and Kraus, Nicolai and Forsberg, Fredrik Nordvall and Xu, Chuangjie},
  year          = 2023,
  month         = {06},
  date          = {2023-06-26},
  booktitle     = {2023 38th {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}} ({{LICS}})},
  pages         = {1--13},
  doi           = {10.1109/LICS56636.2023.10175762},
  eprint        = {2301.10696},
  eprinttype    = {arxiv},
  eprintclass   = {cs, math},
  abstract      = {In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel's interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel's interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the type-theoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.},
  keywords      = {Computer Science - Logic in Computer Science,Mathematics - Logic},
}

@online{Dlicata335/Cohesion-Agda,
  title         = {{Dlicata335/Cohesion-Agda}},
  author        = {Licata, Dan},
  date          = {2017-11-06T03:09:02Z},
  url           = {https://github.com/dlicata335/cohesion-agda},
  origdate      = {2017-11-06T03:08:45Z},
  howpublished  = {{{GitHub}} repository},
}

@article{EKMS93,
  title         = {A {{Primer}} on {{Galois Connections}}},
  author        = {Erné, M. and Koslowski, J. and Melton, A. and Strecker, G. E.},
  year          = 1993,
  journal       = {Annals of the New York Academy of Sciences},
  volume        = 704,
  number        = 1,
  pages         = {103--125},
  doi           = {10.1111/j.1749-6632.1993.tb52513.x},
  issn          = {1749-6632},
  abstract      = {The rudiments of the theory of Galois connections (or residuation theory, as it is sometimes called) are provided, together with many examples and applications. Galois connections occur in profusion and are well known to most mathematicians who deal with order theory; they seem to be less known to topologists. However, because of their ubiquity and simplicity, they (like equivalence relations) can be used as an effective research tool throughout mathematics and related areas. If one recognizes that a Galois connection is involved in a phenomenon that may be relatively complex, then many aspects of that phenomenon immediately become clear, and thus, the whole situation typically becomes much easier to understand.},
  langid        = {english},
  keywords      = {axiality,closure operation,Galois connection,interior operation,polarity},
}

@article{Esc08,
  title         = {Exhaustible sets in higher-type computation},
  author        = {Escardó, Martín Hötzel},
  year          = 2008,
  month         = aug,
  journal       = {Logical Methods in Computer Science},
  publisher     = {Centre pour la Communication Scientifique Directe (CCSD)},
  volume        = 4,
  number        = 3,
  pages         = {3:3, 37},
  doi           = {10.2168/LMCS-4(3:3)2008},
  issn          = {1860-5974},
  eprint        = {0808.0441},
  eprinttype    = {arxiv},
  eprintclass   = {cs},
  primaryclass  = {cs.LO},
  issue         = 3,
}

@article{Esc13,
  title         = {Infinite sets that satisfy the principle of omniscience in any variety of constructive mathematics},
  author        = {Escardó, Martín Hötzel},
  year          = 2013,
  journal       = {The Journal of Symbolic Logic},
  volume        = 78,
  number        = 3,
  pages         = {764--784},
  issn          = {0022-4812,1943-5886},
  mrclass       = {03F50 (03F55)},
  mrnumber      = 3135497,
  mrreviewer    = {Paulo\ Oliva},
}

@online{Esc17YetAnother,
  title         = {Yet another characterization of univalence},
  author        = {Escardó, Martín Hötzel},
  year          = 2017,
  month         = nov,
  date          = {2017-11-18},
  url           = {https://groups.google.com/g/homotopytypetheory/c/FfiZj1vrkmQ/m/GJETdy0AAgAJ},
  howpublished  = {{{Google}} groups forum discussion},
}

@online{Esc19DefinitionsEquivalence,
  title         = {Definitions of Equivalence Satisfying Judgmental/Strict Groupoid Laws?},
  author        = {Escardó, Martín Hötzel},
  year          = 2019,
  month         = {09},
  date          = {2019-09-12},
  url           = {https://groups.google.com/g/homotopytypetheory/c/FfiZj1vrkmQ/m/GJETdy0AAgAJ},
  howpublished  = {{{Google}} groups forum discussion},
}

@article{Esc21,
  title         = {The {{Cantor}}–{{Schröder}}–{{Bernstein Theorem}} for $\infty$-Groupoids},
  author        = {Escardó, Martín Hötzel},
  year          = 2021,
  month         = {09},
  date          = {2021-09-01},
  journal       = {Journal of Homotopy and Related Structures},
  shortjournal  = {J. Homotopy Relat. Struct.},
  volume        = 16,
  number        = 3,
  pages         = {363--366},
  doi           = {10.1007/s40062-021-00284-6},
  issn          = {1512-2891},
  eprint        = {2002.07079},
  eprinttype    = {arxiv},
  eprintclass   = {math},
  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 $\infty$-topos.},
  langid        = {english},
  keywords      = {55U40 03B15,Mathematics - Algebraic Geometry,Mathematics - Logic},
}

@article{Esc21b,
  title         = {Injective types in univalent mathematics},
  author        = {Escardó, Martín Hötzel},
  year          = 2021,
  journal       = {Mathematical Structures in Computer Science},
  volume        = 31,
  number        = 1,
  pages         = {89--111},
  doi           = {10.1017/S0960129520000225},
  issn          = {0960-1295,1469-8072},
  eprint        = {1903.01211},
  archiveprefix = {arXiv},
  primaryclass  = {math.CT},
  url           = {https://martinescardo.github.io/TypeTopology/InjectiveTypes.Article.html},
}

@book{FBL73,
  title         = {Foundations of set theory},
  author        = {Fraenkel, Abraham A. and Bar-Hillel, Yehoshua and Levy, Azriel},
  year          = 1973,
  publisher     = {North-Holland Publishing Co., Amsterdam-London},
  series        = {Studies in Logic and the Foundations of Mathematics},
  volume        = 67,
  pages         = {x+404},
  note          = {With the collaboration of Dirk van Dalen},
  edition       = {revised},
}

@online{Felixwellen/DCHoTT-Agda,
  title         = {{Felixwellen/DCHoTT-Agda}},
  author        = {Cherubini, Felix},
  date          = {2023-08-15T18:08:37Z},
  url           = {https://github.com/felixwellen/DCHoTT-Agda},
  origdate      = {2016-09-12T17:09:29Z},
  abstract      = {Differential cohesion in Homotopy Type Theory by an axiomatized infinitesimal shape modality},
  howpublished  = {{{GitHub}} repository},
}

@article{Frank2020,
  title         = {Interpolating Between Choices for the Approximate Intermediate Value Theorem},
  author        = {Frank, Matthew},
  year          = 2020,
  month         = jul,
  journal       = {Logical Methods in Computer Science},
  publisher     = {Centre pour la Communication Scientifique Directe (CCSD)},
  volume        = {Volume 16, Issue 3},
  doi           = {10.23638/lmcs-16(3:5)2020},
  issn          = {1860-5974},
  url           = {http://dx.doi.org/10.23638/LMCS-16(3:5)2020},
}

@online{GGMS24,
  title         = {The {{Category}} of {{Iterative Sets}} in {{Homotopy Type Theory}} and {{Univalent Foundations}}},
  author        = {Gratzer, Daniel and Gylterud, Håkon and Mörtberg, Anders and Stenholm, Elisabeth},
  year          = 2024,
  month         = {02},
  date          = {2024-02-07},
  eprint        = {2402.04893},
  eprinttype    = {arxiv},
  eprintclass   = {cs, math},
  abstract      = {When working in Homotopy Type Theory and Univalent Foundations, the traditional role of the category of sets, Set, is replaced by the category hSet of homotopy sets (h-sets); types with h-propositional identity types. Many of the properties of Set hold for hSet ((co)completeness, exactness, local cartesian closure, etc.). Notably, however, the univalence axiom implies that Ob(hSet) is not itself an h-set, but an h-groupoid. This is expected in univalent foundations, but it is sometimes useful to also have a stricter universe of sets, for example when constructing internal models of type theory. In this work, we equip the type of iterative sets V0, due to Gylterud (2018) as a refinement of the pioneering work of Aczel (1978) on universes of sets in type theory, with the structure of a Tarski universe and show that it satisfies many of the good properties of h-sets. In particular, we organize V0 into a (non-univalent strict) category and prove that it is locally cartesian closed. This enables us to organize it into a category with families with the structure necessary to model extensional type theory internally in HoTT/UF. We do this in a rather minimal univalent type theory with W-types, in particular we do not rely on any HITs, or other complex extensions of type theory. Furthermore, the construction of V0 and the model is fully constructive and predicative, while still being very convenient to work with as the decoding from V0 into h-sets commutes definitionally for all type constructors. Almost all of the paper has been formalized in Agda using the agda-unimath library of univalent mathematics.},
  pubstate      = {preprint},
  keywords      = {Computer Science - Logic in Computer Science,Mathematics - Logic},
}

@article{GHK22,
  title         = {∞-Operads as Analytic Monads},
  author        = {Gepner, David and Haugseng, Rune and Kock, Joachim},
  year          = 2021,
  month         = {04},
  journal       = {International Mathematics Research Notices},
  volume        = 2022,
  number        = 16,
  pages         = {12516--12624},
  doi           = {10.1093/imrn/rnaa332},
  issn          = {1073-7928},
}

@article{GK12,
  title         = {Polynomial functors and polynomial monads},
  author        = {Gambino, Nicola and Kock, Joachim},
  year          = 2012,
  month         = sep,
  journal       = {Mathematical Proceedings of the Cambridge Philosophical Society},
  publisher     = {Cambridge University Press (CUP)},
  volume        = 154,
  number        = 1,
  pages         = {153–192},
  doi           = {10.1017/s0305004112000394},
  issn          = {1469-8064},
}

@book{Johnstone02,
  title         = {Sketches of an Elephant a Topos Theory Compendium},
  author        = {Johnstone, Peter T},
  year          = 2002,
  month         = sep,
  date          = {2002-09},
  publisher     = {Oxford University Press},
  doi           = {10.1093/oso/9780198515982.001.0001},
  isbn          = {978-0-19-851598-2},
  abstract      = {Topos Theory is a subject that stands at the junction of geometry, mathematical logic and theoretical computer science, and it derives much of its power from the interplay of ideas drawn from these different areas. Because of this, an account of topos theory which approaches the subject from one particular direction can only hope to give a partial picture; the aim of this compendium is to present as comprehensive an account as possible of all the main approaches and thereby to demonstrate the overall unity of the subject. The material is organized in such a way that readers interested in following a particular line of approach may do so by starting at an appropriate point in the text.},
}

@article{KECA17,
  title         = {{Notions of Anonymous Existence in {{Martin-L\"of}} Type Theory}},
  author        = {Nicolai Kraus and Martín Escardó and Thierry Coquand and Thorsten Altenkirch},
  year          = 2017,
  month         = {03},
  journal       = {{Logical Methods in Computer Science}},
  volume        = 13,
  doi           = {10.23638/LMCS-13(1:15)2017},
  eprint        = {1610.03346},
  eprinttype    = {arxiv},
  eprintclass   = {cs},
  url           = {https://lmcs.episciences.org/3217},
  issue         = 1,
  keywords      = {Computer Science - Logic in Computer Science ; 03B15 ; F.4.1},
}

@article{König1906,
  title         = {Sur la théorie des ensembles},
  author        = {J. König},
  year          = 1906,
  journal       = {Comptes Rendus Hebdomadaires des Séances de l'Académie des Sciences},
  volume        = 143,
  pages         = {110--112},
  url           = {https://gallica.bnf.fr/ark:/12148/bpt6k30977.image.f110.langEN},
  language      = {french},
}

@inproceedings{Kraus15,
  title         = {{The General Universal Property of the Propositional Truncation}},
  author        = {Kraus, Nicolai},
  year          = 2015,
  booktitle     = {20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  publisher     = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address       = {Dagstuhl, Germany},
  series        = {Leibniz International Proceedings in Informatics (LIPIcs)},
  volume        = 39,
  pages         = {111--145},
  doi           = {10.4230/LIPIcs.TYPES.2014.111},
  isbn          = {978-3-939897-88-0},
  issn          = {1868-8969},
  editor        = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu},
  urn           = {urn:nbn:de:0030-drops-54944},
  annote        = {Keywords: coherence conditions, propositional truncation, Reedy limits, universal property, well-behaved constancy},
}

@book{Kunen11,
  title         = {Set theory},
  author        = {Kunen, Kenneth},
  year          = 2011,
  publisher     = {College Publications, London},
  series        = {Studies in Logic (London)},
  volume        = 34,
  pages         = {viii+401},
  isbn          = {978-1-84890-050-9},
}

@inproceedings{KvR19,
  title         = {{Path Spaces of Higher Inductive Types in Homotopy Type Theory}},
  author        = {Kraus, Nicolai and von Raumer, Jakob},
  year          = 2019,
  booktitle     = {Proceedings of the 34th {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}}},
  location      = {Vancouver, Canada},
  publisher     = {IEEE Press},
  series        = {LICS '19},
  eprint        = {1901.06022},
  eprinttype    = {arxiv},
  eprintclass   = {cs, math},
  abstract      = {The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove a theorem about equality types of coequalizers and pushouts, reminiscent of an induction principle and without any restrictions on the truncation levels. This result makes it possible to reason directly about certain equality types and to streamline existing proofs by eliminating the necessity of auxiliary constructions. To demonstrate this, we give a very short argument for the calculation of the fundamental group of the circle (Licata and Shulman [1]), and for the fact that pushouts preserve embeddings. Further, our development suggests a higher version of the Seifert-van Kampen theorem, and the set-truncation operator maps it to the standard Seifert-van Kampen theorem (due to Favonia and Shulman [2]). We provide a formalization of the main technical results in the proof assistant Lean.},
  articleno     = 7,
  numpages      = 13,
}

@misc{Lavenir23,
  title         = {{{Hilton–Milnor's}} theorem in $\infty$-topoi},
  author        = {Samuel Lavenir},
  year          = 2023,
  eprint        = {2312.12370},
  archiveprefix = {arXiv},
  primaryclass  = {math.AT},
}

@article{Ljungström24,
  title         = {Symmetric monoidal smash products in homotopy type theory},
  author        = {Ljungström, Axel},
  year          = 2024,
  month         = oct,
  journal       = {Mathematical Structures in Computer Science},
  publisher     = {Cambridge University Press (CUP)},
  volume        = 34,
  number        = 9,
  pages         = {985–1007},
  doi           = {10.1017/s0960129524000318},
  issn          = {1469-8072},
}

@misc{Lord25,
  title         = {Easy Parametricity},
  author        = {Jem Lord},
  year          = 2025,
  url           = {https://hott-uf.github.io/2025/abstracts/HoTTUF\%5F2025\%5Fpaper\%5F21.pdf},
}

@book{Lurie09,
  title         = {Higher Topos Theory},
  author        = {Jacob Lurie},
  year          = 2009,
  publisher     = {Princeton University Press},
  isbn          = 9780691140490,
  url           = {https://www.math.ias.edu/~lurie/papers/highertopoi.pdf},
}

@incollection{Makkai98,
  title         = {Towards a categorical foundation of mathematics},
  author        = {Makkai, M.},
  year          = 1998,
  booktitle     = {Logic {C}olloquium '95 ({H}aifa)},
  publisher     = {Springer, Berlin},
  series        = {Lecture Notes Logic},
  volume        = 11,
  pages         = {153--190},
  doi           = {10.1007/978-3-662-22108-2\_11},
  isbn          = {3-540-63994-2},
  mrclass       = {03B15 (00A30 03A05 03G30 18A15 18D05)},
  mrnumber      = 1678360,
  mrreviewer    = {Peter\ Johnstone},
}

@book{May12,
  title         = {More {{Concise Algebraic Topology}}: {{Localization}}, {{Completion}}, and {{Model Categories}}},
  shorttitle    = {More {{Concise Algebraic Topology}}},
  author        = {May, J. P. and Ponto, K.},
  year          = 2012,
  month         = {02},
  date          = {2012-02},
  publisher     = {University of Chicago Press},
  isbn          = {978-0-226-51178-8},
  abstract      = {With firm foundations dating only from the 1950s, algebraic topology is a relatively young area of mathematics. There are very few textbooks that treat fundamental topics beyond a first course, and many topics now essential to the field are not treated in any textbook. J. Peter May’s A Concise Course in Algebraic Topology addresses the standard first course material, such as fundamental groups, covering spaces, the basics of homotopy theory, and homology and cohomology. In this sequel, May and his coauthor, Kathleen Ponto, cover topics that are essential for algebraic topologists and others interested in algebraic topology, but that are not treated in standard texts. They focus on the localization and completion of topological spaces, model categories, and Hopf algebras. The first half of the book sets out the basic theory of localization and completion of nilpotent spaces, using the most elementary treatment the authors know of. It makes no use of simplicial techniques or model categories, and it provides full details of other necessary preliminaries. With these topics as motivation, most of the second half of the book sets out the theory of model categories, which is the central organizing framework for homotopical algebra in general. Examples from topology and homological algebra are treated in parallel. A short last part develops the basic theory of bialgebras and Hopf algebras.},
  langid        = {english},
  pagetotal     = 544,
  keywords      = {Mathematics / Algebra / Abstract,Mathematics / General,Mathematics / Topology},
}

@book{May99,
  title         = {A {{Concise Course}} in {{Algebraic Topology}}},
  author        = {May, J. P.},
  year          = 1999,
  month         = {09},
  date          = {1999-09},
  publisher     = {University of Chicago Press},
  isbn          = {978-0-226-51183-2},
  url           = {https://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf},
  abstract      = {Algebraic topology is a basic part of modern mathematics, and some knowledge of this area is indispensable for any advanced work relating to geometry, including topology itself, differential geometry, algebraic geometry, and Lie groups. This book provides a detailed treatment of algebraic topology both for teachers of the subject and for advanced graduate students in mathematics either specializing in this area or continuing on to other fields.  J. Peter May's approach reflects the enormous internal developments within algebraic topology over the past several decades, most of which are largely unknown to mathematicians in other fields. But he also retains the classical presentations of various topics where appropriate. Most chapters end with problems that further explore and refine the concepts presented. The final four chapters provide sketches of substantial areas of algebraic topology that are normally omitted from introductory texts, and the book concludes with a list of suggested readings for those interested in delving further into the field.},
  langid        = {english},
  pagetotal     = 262,
  keywords      = {Mathematics / General,Mathematics / Topology},
}

@article{McAl74,
  title         = {Groups, {{Semilattices}} and {{Inverse Semigroups}}},
  author        = {McAlister, D. B.},
  year          = 1974,
  journal       = {Transactions of the American Mathematical Society},
  publisher     = {American Mathematical Society},
  volume        = 192,
  pages         = {227--244},
  doi           = {10.2307/1996831},
  issn          = {0002-9947},
  eprint        = 1996831,
  eprinttype    = {jstor},
  abstract      = {An inverse semigroup S is called proper if the equations ea = e = e2 together imply a2 = a for each a, e ∈ S. In this paper a construction is given for a large class of proper inverse semigroups in terms of groups and partially ordered sets; the semigroups in this class are called P-semigroups. It is shown that every inverse semigroup divides a P-semigroup in the sense that it is the image, under an idempotent separating homomorphism, of a full subsemigroup of a P-semigroup. Explicit divisions of this type are given for ω-bisimple semigroups, proper bisimple inverse semigroups, semilattices of groups and Brandt semigroups.},
}

@article{Mil84,
  title         = {The {{Sullivan Conjecture}} on {{Maps}} from {{Classifying Spaces}}},
  author        = {Miller, Haynes},
  year          = 1984,
  journal       = {Annals of Mathematics},
  publisher     = {Annals of Mathematics},
  volume        = 120,
  number        = 1,
  pages         = {39--87},
  doi           = {10.2307/2007071},
  issn          = {0003-486X},
  eprint        = 2007071,
  eprinttype    = {jstor},
}

@book{MM94,
  title         = {Sheaves in {{Geometry}} and {{Logic}}: {{A First Introduction}} to {{Topos Theory}}},
  shorttitle    = {Sheaves in {{Geometry}} and {{Logic}}},
  author        = {Mac Lane, Saunders and Moerdijk, Ieke},
  year          = 1994,
  location      = {New York, NY},
  publisher     = {Springer New York},
  series        = {Universitext},
  doi           = {10.1007/978-1-4612-0927-0},
  isbn          = {978-0-387-97710-2 978-1-4612-0927-0},
  langid        = {english},
  edition       = {1st ed. 1994.},
  keywords      = {Geometry ; K-theory ; Logic Symbolic and mathematical},
}

@article{MP87,
  title         = {Inverse Semigroups and Extensions of Groups by Semilattices},
  author        = {Margolis, S. W and Pin, J. E},
  year          = 1987,
  month         = oct,
  date          = {1987-10-15},
  journal       = {Journal of Algebra},
  shortjournal  = {Journal of Algebra},
  volume        = 110,
  number        = 2,
  pages         = {277--297},
  doi           = {10.1016/0021-8693(87)90046-9},
  issn          = {0021-8693},
}

@online{MR23,
  title         = {Delooping the Sign Homomorphism in Univalent Mathematics},
  author        = {Mangel, Éléonore and Rijke, Egbert},
  year          = 2023,
  month         = {01},
  date          = {2023-01-24},
  eprint        = {2301.10011},
  eprinttype    = {arxiv},
  eprintclass   = {math},
  abstract      = {In univalent mathematics there are at least two equivalent ways to present the category of groups. Groups presented in their usual algebraic form are called abstract groups, and groups presented as pointed connected $1$-types are called concrete groups. Since these two descriptions of the category of groups are equivalent, we find that every algebraic group corresponds uniquely to a concrete group -- its delooping -- and that each abstract group homomorphisms corresponds uniquely to a pointed map between concrete groups. The $n$-th abstract symmetric group $S_n$ of all bijections $[n]\simeq [n]$, for instance, corresponds to the concrete group of all $n$-element types. The sign homomorphism from $S_n$ to $S_2$ should therefore correspond to a pointed map from the type $BS_n$ of all $n$-element types to the type $BS_2$ of all $2$-element types. Making use of the univalence axiom, we characterize precisely when a pointed map $BS_n\to_\ast BS_2$ is a delooping of the sign homomorphism. Then we proceed to give several constructions of the delooping of the sign homomorphism. Notably, the construction following a method of Cartier can be given without reference to the sign homomorphism. Our results are formalized in the agda-unimath library.},
  pubstate      = {preprint},
  keywords      = {20B30 03B15,Mathematics - Group Theory,Mathematics - Logic},
}

@book{MRR88,
  title         = {A {{Course}} in {{Constructive Algebra}}},
  author        = {Mines, Ray and Richman, Fred and Ruitenburg, Wim},
  year          = 1988,
  location      = {New York, NY},
  publisher     = {Springer New York},
  series        = {Universitext},
  doi           = {10.1007/978-1-4419-8640-5},
  isbn          = {978-0-387-96640-3 978-1-4419-8640-5},
  url           = {http://link.springer.com/10.1007/978-1-4419-8640-5},
  editorb       = {Ewing, J. and Gehring, F. W. and Halmos, P. R.},
  editorbtype   = {redactor},
}

@misc{MS04,
  title         = {Parametrized homotopy theory},
  author        = {J. P. May and J. Sigurdsson},
  year          = 2004,
  eprint        = {math/0411656},
  archiveprefix = {arXiv},
  primaryclass  = {math.AT},
}

@misc{Mye21,
  title         = {Modal Fracture of Higher Groups},
  author        = {David Jaz Myers},
  year          = 2021,
  eprint        = {2106.15390},
  archiveprefix = {arXiv},
  eprintclass   = {math},
  primaryclass  = {math.CT},
}

@online{oeis,
  title         = {The {{On-Line Encyclopedia}} of {{Integer Sequences}}},
  author        = {OEIS Foundation Inc.},
  date          = 1996,
  url           = {https://oeis.org},
  citeas        = {OEIS},
  howpublished  = {website},
}

@online{Palmgren14VariantsCwF,
  title         = {Variants of categories with families and their formalization (work in progress)},
  author        = {Erik Palmgren},
  year          = 2014,
  date          = {2014-12-11},
  location      = {Göteborg},
  url           = {https://staff.math.su.se/palmgren/ErikP\%5FVariants\%5FCWF.pdf},
  note          = {Type theory and formalization of mathematics workshop},
  institution   = {Stockholm University, Department of Mathematics},
}

@phdthesis{Qui16,
  title         = {{{Lawvere–Tierney}} sheafification in Homotopy Type Theory},
  author        = {Quirin, Kevin},
  year          = 2016,
  month         = dec,
  number        = {2016EMNA0298},
  url           = {https://kevinquirin.github.io/thesis/main.pdf},
  school        = {École des Mines de Nantes},
  abstract      = {The main goal of this thesis is to define an extension of Gödel not-not translation to all truncated types, in the setting of homotopy type theory. This goal will use some existing theories, like Lawvere–Tierney sheaves theory in toposes, we will adapt in the setting of homotopy type theory. In particular, we will define a Lawvere–Tierney sheafification functor, which is the main theorem presented in this thesis. To define it, we will need some concepts, either already defined in type theory, either not existing yet. In particular, we will define a theory of colimits over graphs as well as their truncated version, and the notion of truncated modalities, based on the existing definition of modalities. Almost all the result presented in this thesis are formalized with the proof assistant Coq together with the library [HoTT/Coq].},
  langid        = {english},
}

@online{Rezk10HomotopyToposes,
  title         = {Toposes and homotopy toposes},
  author        = {Rezk, Charles},
  year          = 2010,
  month         = {01},
  url           = {https://rezk.web.illinois.edu/homotopy-topos-sketch.pdf},
  version       = {0.15},
}

@book{Rie17,
  title         = {Category {{Theory}} in {{Context}}},
  author        = {Riehl, Emily},
  year          = 2017,
  month         = {03},
  date          = {2017-03-09},
  publisher     = {Courier Dover Publications},
  isbn          = {978-0-486-82080-4},
  url           = {https://math.jhu.edu/~eriehl/context.pdf},
  abstract      = {"The book is extremely pleasant to read, with masterfully crafted exercises and examples that create a beautiful and unique thread of presentation leading the reader safely into the wonderfully rich, expressive, and powerful theory of categories." — The Math Association Category theory has provided the foundations for many of the twentieth century's greatest advances in pure mathematics. This concise, original text for a one-semester course on the subject is derived from courses that author Emily Riehl taught at Harvard and Johns Hopkins Universities. The treatment introduces the essential concepts of category theory: categories, functors, natural transformations, the Yoneda lemma, limits and colimits, adjunctions, monads, and other topics. Suitable for advanced undergraduates and graduate students in mathematics, the text provides tools for understanding and attacking difficult problems in algebra, number theory, algebraic geometry, and algebraic topology. Drawing upon a broad range of mathematical examples from the categorical perspective, the author illustrates how the concepts and constructions of category theory arise from and illuminate more basic mathematical ideas. Prerequisites are limited to familiarity with some basic set theory and logic.},
  langid        = {english},
  pagetotal     = 273,
  keywords      = {Mathematics / Logic},
}

@book{Rie22,
  title         = {Elements of $\infty$-{{Category Theory}}},
  author        = {Riehl, Emily and Verity, Dominic},
  year          = 2022,
  location      = {Cambridge},
  publisher     = {Cambridge University Press},
  series        = {Cambridge {{Studies}} in {{Advanced Mathematics}}},
  doi           = {10.1017/9781108936880},
  isbn          = {978-1-108-83798-9},
  url           = {https://math.jhu.edu/~eriehl/elements.pdf},
  abstract      = {The language of $\infty$-categories provides an insightful new way of expressing many results in higher-dimensional mathematics but can be challenging for the uninitiated. To explain what exactly an $\infty$-category is requires various technical models, raising the question of how they might be compared. To overcome this, a model-independent approach is desired, so that theorems proven with any model would apply to them all. This text develops the theory of $\infty$-categories from first principles in a model-independent fashion using the axiomatic framework of an $\infty$-cosmos, the universe in which $\infty$-categories live as objects. An $\infty$-cosmos is a fertile setting for the formal category theory of $\infty$-categories, and in this way the foundational proofs in $\infty$-category theory closely resemble the classical foundations of ordinary category theory. Equipped with exercises and appendices with background material, this first introduction is meant for students and researchers who have a strong foundation in classical 1-category theory.},
}

@online{Rij17,
  title         = {The Join Construction},
  author        = {Rijke, Egbert},
  year          = 2017,
  month         = {01},
  date          = {2017-01-25},
  eprint        = {1701.07538},
  eprinttype    = {arxiv},
  eprintclass   = {math},
  urldate       = {2023-02-05},
  abstract      = {In homotopy type theory we can define the join of maps as a binary operation on maps with a common co-domain. This operation is commutative, associative, and the unique map from the empty type into the common codomain is a neutral element. Moreover, we show that the idempotents of the join of maps are precisely the embeddings, and we prove the `join connectivity theorem', which states that the connectivity of the join of maps equals the join of the connectivities of the individual maps. We define the image of a map $f:A\to X$ in $U$ via the join construction, as the colimit of the finite join powers of $f$. The join powers therefore provide approximations of the image inclusion, and the join connectivity theorem implies that the approximating maps into the image increase in connectivity. A modified version of the join construction can be used to show that for any map $f:A\to X$ in which $X$ is only assumed to be locally small, the image is a small type. We use the modified join construction to give an alternative construction of set-quotients, the Rezk completion of a precategory, and we define the $n$-truncation for any $n:\mathbb{N}$. Thus we see that each of these are definable operations on a univalent universe for Martin-L\"of type theory with a natural numbers object, that is moreover closed under homotopy coequalizers.},
  pubstate      = {preprint},
  keywords      = {Mathematics - Category Theory,Mathematics - Logic},
}

@phdthesis{Rij19,
  title         = {Classifying {{Types}}},
  author        = {Rijke, Egbert},
  year          = 2019,
  month         = {06},
  date          = {2019-06-22},
  eprint        = {1906.09435},
  eprinttype    = {arxiv},
  eprintclass   = {math},
  abstract      = {The study of homotopy theoretic phenomena in the language of type theory is sometimes loosely called `synthetic homotopy theory'. Homotopy theory in type theory is only one of the many aspects of homotopy type theory, which also includes the study of the set theoretic semantics (models of homotopy type theory and univalence in a meta-theory of sets or categories), type theoretic semantics (internal models of homotopy type theory), and computational semantics, as well as the study of various questions in the internal language of homotopy type theory which are not necessarily motivated by homotopy theory, or questions related to the development of formalized libraries of mathematics based on homotopy type theory. This thesis concerns the development of synthetic homotopy theory.},
  pubstate      = {preprint},
  keywords      = {Mathematics - Logic},
  school        = {Carnegie Mellon University},
}

@book{Rij22,
  title         = {Introduction to {{Homotopy Type Theory}}},
  author        = {Rijke, Egbert},
  year          = 2022,
  month         = dec,
  date          = {2022-12-21},
  publisher     = {},
  eprint        = {2212.11082},
  eprinttype    = {arxiv},
  eprintclass   = {math},
  abstract      = {This is an introductory textbook to univalent mathematics and homotopy type theory, a mathematical foundation that takes advantage of the structural nature of mathematical definitions and constructions. It is common in mathematical practice to consider equivalent objects to be the same, for example, to identify isomorphic groups. In set theory it is not possible to make this common practice formal. For example, there are as many distinct trivial groups in set theory as there are distinct singleton sets. Type theory, on the other hand, takes a more structural approach to the foundations of mathematics that accommodates the univalence axiom. This, however, requires us to rethink what it means for two objects to be equal. This textbook introduces the reader to Martin-L\"of's dependent type theory, to the central concepts of univalent mathematics, and shows the reader how to do mathematics from a univalent point of view. Over 200 exercises are included to train the reader in type theoretic reasoning. The book is entirely self-contained, and in particular no prior familiarity with type theory or homotopy theory is assumed.},
  langid        = {english},
}

@online{Rij22draft,
  title         = {Introduction to {{Homotopy Type Theory}}},
  author        = {Rijke, Egbert},
  year          = 2022,
  url           = {https://raw.githubusercontent.com/martinescardo/HoTTEST-Summer-School/main/HoTT/hott-intro.pdf},
  pubstate      = {draft},
}

@article{RSS20,
  title         = {Modalities in Homotopy Type Theory},
  author        = {Rijke, Egbert and Shulman, Michael and Spitters, Bas},
  year          = 2020,
  month         = {01},
  date          = {2020-01-08},
  journal       = {Logical Methods in Computer Science},
  publisher     = {Episciences.org},
  volume        = {Volume 16, Issue 1},
  doi           = {10.23638/LMCS-16(1:2)2020},
  issn          = {1860-5974},
  eprint        = {1706.07526},
  eprinttype    = {arxiv},
  eprintclass   = {cs, math},
  url           = {https://lmcs.episciences.org/6015},
  abstract      = {Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a "localization" higher inductive type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.},
  keywords      = {Computer Science - Logic in Computer Science,F.3.1,F.3.1 F.4.1,F.4.1,Mathematics - Category Theory,Mathematics - Logic},
}

@online{Shu14SplittingIdempotents,
  title         = {Splitting {{Idempotents}}},
  author        = {Shulman, Mike},
  year          = 2014,
  month         = dec,
  date          = {2014-12-08T07:44:32+00:00},
  url           = {https://homotopytypetheory.org/2014/12/08/splitting-idempotents/},
  abstract      = {A few days ago Martin Escardo asked me “Do idempotents split in HoTT”? This post is an answer to that question.},
  langid        = {english},
  organization  = {Homotopy Type Theory},
  howpublished  = {Blog post},
}

@online{Shu14UniversalProperties,
  title         = {Universal Properties without Function Extensionality},
  author        = {Shulman, Mike},
  year          = 2014,
  month         = nov,
  date          = {2014-11-02T04:55:50+00:00},
  url           = {https://homotopytypetheory.org/2014/11/02/universal-properties-without-function-extensionality/},
  abstract      = {A universal property, in the sense of category theory, generally expresses that a map involving hom-sets, induced by composition with some canonical map(s), is an isomorphism. In type theory we exp…},
  langid        = {english},
  organization  = {Homotopy Type Theory},
  howpublished  = {Blog post},
}

@article{Shu15,
  title         = {Univalence for inverse diagrams and homotopy canonicity},
  author        = {Shulman, Michael},
  year          = 2015,
  month         = {06},
  date          = {2015-06},
  journal       = {Mathematical Structures in Computer Science},
  volume        = 25,
  number        = 5,
  pages         = {1203--1277},
  doi           = {10.1017/S0960129514000565},
  issn          = {0960-1295, 1469-8072},
  eprint        = {1203.3253},
  eprinttype    = {arxiv},
  eprintclass   = {math},
  rights        = {https://www.cambridge.org/core/terms},
  abstract      = {We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory on inverse diagrams, and relies on the fact that Reedy fibrant diagrams correspond to contexts of a certain shape in type theory. This has two main applications. First, by considering inverse diagrams in Voevodsky's univalent model in simplicial sets, we obtain new models of univalence in a number of (∞, 1)-toposes; this answers a question raised at the Oberwolfach workshop on homotopical type theory. Second, by gluing the syntactic category of univalent type theory along its global sections functor to groupoids, we obtain a partial answer to Voevodsky's homotopy-canonicity conjecture: in 1-truncated type theory with one univalent universe of sets, any closed term of natural number type is homotopic to a numeral.},
  langid        = {english},
}

@article{Shu17,
  title         = {Idempotents in Intensional Type Theory},
  author        = {Shulman, Michael},
  year          = 2017,
  month         = {04},
  date          = {2017-04-27},
  journal       = {Logical Methods in Computer Science},
  publisher     = {Episciences.org},
  volume        = 12,
  pages         = {1--24},
  doi           = {10.2168/LMCS-12(3:9)2016},
  issn          = {1860-5974},
  eprint        = {1507.03634},
  eprinttype    = {arxiv},
  eprintclass   = {math},
  primaryclass  = {math.LO},
  issue         = 3,
  abstract      = {We study idempotents in intensional Martin-L\"of type theory, and in particular the question of when and whether they split. We show that in the presence of propositional truncation and Voevodsky's univalence axiom, there exist idempotents that do not split; thus in plain MLTT not all idempotents can be proven to split. On the other hand, assuming only function extensionality, an idempotent can be split if and only if its witness of idempotency satisfies one extra coherence condition. Both proofs are inspired by parallel results of Lurie in higher category theory, showing that ideas from higher category theory and homotopy theory can have applications even in ordinary MLTT. Finally, we show that although the witness of idempotency can be recovered from a splitting, the one extra coherence condition cannot in general; and we construct "the type of fully coherent idempotents", by splitting an idempotent on the type of partially coherent ones. Our results have been formally verified in the proof assistant Coq.},
}

@article{Shu18,
  title         = {{{Brouwer's}} Fixed-Point Theorem in Real-Cohesive Homotopy Type Theory},
  author        = {Shulman, Michael},
  year          = 2018,
  month         = {06},
  date          = {2018-06},
  journal       = {Mathematical Structures in Computer Science},
  volume        = 28,
  number        = 6,
  pages         = {856--941},
  doi           = {10.1017/S0960129517000147},
  issn          = {0960-1295, 1469-8072},
  eprint        = {1509.07584},
  eprinttype    = {arxiv},
  eprintclass   = {math},
  abstract      = {We combine homotopy type theory with axiomatic cohesion, expressing the latter internally with a version of ‘adjoint logic’ in which the discretization and codiscretization modalities are characterized using a judgemental formalism of ‘crisp variables.’ This yields type theories that we call ‘spatial’ and ‘cohesive,’ in which the types can be viewed as having independent topological and homotopical structure. These type theories can then be used to study formally the process by which topology gives rise to homotopy theory (the ‘fundamental $\infty$-groupoid’ or ‘shape’), disentangling the ‘identifications’ of homotopy type theory from the ‘continuous paths’ of topology. In a further refinement called ‘real-cohesion,’ the shape is determined by continuous maps from the real numbers, as in classical algebraic topology. This enables us to reproduce formally some of the classical applications of homotopy theory to topology. As an example, we prove Brouwer's fixed-point theorem.},
  langid        = {english},
  keywords      = {Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic},
}

@article{Sto87,
  title         = {{{Dedekind}} finiteness in topoi},
  author        = {Lawrence Neff Stout},
  year          = 1987,
  journal       = {Journal of Pure and Applied Algebra},
  volume        = 49,
  number        = 1,
  pages         = {219--225},
  doi           = {10.1016/0022-4049(87)90130-7},
  issn          = {0022-4049},
  abstract      = {A Dedekind finite object in a topos is an object such that any monic endomorphism is an epimorphism. This paper proves the basic properties of Dedekind finiteness and then gives examples which show that the class of Dedekind finite objects is not closed under quotients, subobjects, exponentiation, or finite powerobjects. Examples also show that having no nontrivial epic endomorphisms is distinct from Dedekind finiteness.},
}

@inproceedings{SvDR20,
  title         = {Sequential {{Colimits}} in {{Homotopy Type Theory}}},
  author        = {Sojakova, Kristina and van Doorn, Floris and Rijke, Egbert},
  year          = 2020,
  month         = {07},
  date          = {2020-07-08},
  booktitle     = {Proceedings of the 35th {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}}},
  location      = {New York, NY, USA},
  publisher     = {Association for Computing Machinery},
  series        = {{{LICS}} '20},
  pages         = {845--858},
  doi           = {10.1145/3373718.3394801},
  isbn          = {978-1-4503-7104-9},
  abstract      = {Sequential colimits are an important class of higher inductive types. We present a self-contained and fully formalized proof of the conjecture that in homotopy type theory sequential colimits appropriately commute with Σ-types. This result allows us to give short proofs of a number of useful corollaries, some of which were conjectured in other works: the commutativity of sequential colimits with identity types, with homotopy fibers, loop spaces, and truncations, and the preservation of the properties of truncatedness and connectedness under sequential colimits. Our entire development carries over to (∞, 1)-toposes using Shulman's recent interpretation of homotopy type theory into these structures.},
  keywords      = {higher inductive types,homotopy type theory,sequential colimits},
}

@misc{Swan24,
  title         = {Oracle modalities},
  author        = {Swan, Andrew W},
  year          = 2024,
  eprint        = {2406.05818},
  archiveprefix = {arXiv},
  eprintclass   = {math},
  primaryclass  = {math.LO},
}

@book{SymmetryBook,
  title         = {Symmetry},
  author        = {Bezem, Marc and Buchholtz, Ulrik and Cagne, Pierre and Dundas, Bjørn Ian and Grayson, Daniel R},
  year          = 2023,
  month         = {06},
  date          = {2023-06-07},
  publisher     = {},
  url           = {https://unimath.github.io/SymmetryBook/book.pdf},
  langid        = {english},
}

@online{TypeTopology,
  title         = {{TypeTopology}},
  author        = {Escardó, Martín Hötzel and {contributors}},
  url           = {https://github.com/martinescardo/TypeTopology},
  note          = {{{Agda}} development},
  citeas        = {Esc},
  howpublished  = {{{GitHub}} repository},
}

@book{UF13,
  title         = {Homotopy {{Type Theory}}: {{Univalent Foundations}} of {{Mathematics}}},
  shorttitle    = {Homotopy {{Type Theory}}},
  author        = {{The Univalent Foundations Program}},
  year          = 2013,
  publisher     = {},
  address       = {Institute for Advanced Study},
  eprint        = {1308.0729},
  eprinttype    = {arxiv},
  eprintclass   = {math},
  url           = {https://homotopytypetheory.org/book/},
  langid        = {english},
  citeas        = {UF13},
}

@article{Voe10,
  title         = {Unstable Motivic Homotopy Categories in {{Nisnevich}} and Cdh-Topologies},
  author        = {Voevodsky, Vladimir},
  year          = 2010,
  month         = {08},
  date          = {2010-08-01},
  journal       = {Journal of Pure and Applied Algebra},
  shortjournal  = {Journal of Pure and Applied Algebra},
  volume        = 214,
  number        = 8,
  pages         = {1399--1406},
  doi           = {10.1016/j.jpaa.2009.11.005},
  issn          = {0022-4049},
  eprint        = {0805.4576},
  eprinttype    = {arxiv},
  eprintclass   = {math},
  url           = {https://www.sciencedirect.com/science/article/pii/S0022404909002643},
  abstract      = {The motivic homotopy categories can be defined with respect to different topologies and different underlying categories of schemes. For a number of reasons (mainly because of the Gluing Theorem) the motivic homotopy category of smooth schemes with respect to the Nisnevich topology plays a distinguished role but in some cases it is desirable to be able to work with all schemes instead of the smooth ones. In this paper we prove that, under the resolution of singularities assumption, the unstable motivic homotopy category of all schemes over a field with respect to the cdh-topology is almost equivalent to the unstable motivic homotopy category of smooth schemes over the same field with respect to the Nisnevich topology.},
  keywords      = {14F42,Mathematics - Algebraic Geometry},
}

@misc{Warn23draft,
  title         = {Path Spaces of Pushouts},
  author        = {Wärn, David},
  year          = 2023,
  month         = {04},
  date          = {4/21/2023, 12:04:00 AM},
  url           = {https://dwarn.se/po-paths.pdf},
  howpublished  = {E-mail},
  abstract      = {Working in homotopy type theory, we describe path spaces of pushouts as sequential colimits of pushouts. This gives a higher Seifert–van Kampen theorem. We demonstrate the utility of this description by showing that any pushout of 0-types is a 1-type, settling a long-standing open question in homotopy type theory. Our construction can be interpreted in any higher category with pullbacks, finite colimits satisfying descent, and sequential colimits.},
  langid        = {english},
}

@online{Warn24,
  title         = {Path Spaces of Pushouts},
  author        = {Wärn, David},
  year          = 2024,
  month         = {02},
  date          = {2024-02-19},
  eprint        = {2402.12339},
  eprinttype    = {arxiv},
  eprintclass   = {math},
  urldate       = {2024-02-26},
  abstract      = {Given a span of spaces, one can form the homotopy pushout and then take the homotopy pullback of the resulting cospan. We give a concrete description of this pullback as the colimit of a sequence of approximations, using what we call the zigzag construction. We also obtain a description of loop spaces of homotopy pushouts. Using the zigzag construction, we reproduce generalisations of the Blakers-Massey theorem and fundamental results from Bass-Serre theory. We also describe the loop space of a wedge and show that it splits after suspension. Our construction can be interpreted in a large class of $(\infty,1)$-categories and in homotopy type theory, where it resolves the long-standing open problem of showing that a pushout of 0-types is 1-truncated. The zigzag construction is closely related to the James construction, but works in greater generality.},
  pubstate      = {preprint},
  keywords      = {Mathematics - Algebraic Topology,Mathematics - Category Theory},
}