Higher Structures in Homotopy Type Theory
From MaRDI portal
Publication:6075425
DOI10.1007/978-3-030-15655-8_7zbMath1528.03105arXiv1807.02177OpenAlexW2836615843MaRDI QIDQ6075425
Publication date: 20 September 2023
Published in: Synthese Library (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1807.02177
Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)
Related Items
Cites Work
- Unnamed Item
- Unnamed Item
- Quillen adjunctions induce adjunctions of quasicategories
- Quasi-unital \(\infty\)-categories
- Homotopy type theory in Lean
- Meaning explanations at higher dimension
- Univalent foundations as structuralist foundations
- Univalence as a principle of logic
- Homotopy invariant algebraic structures on topological spaces
- Quasi-categories and Kan complexes
- Homotopical algebra
- Cohomologie modulo 2 des complexes d'Eilenberg-MacLane
- Model Categories of Diagram Spectra
- Type theory in type theory using quotient inductive types
- Higher Homotopies in a Hierarchy of Univalent Universes
- Partiality, Revisited
- A type theory for synthetic $\infty$-categories
- ABSTRACT HOMOTOPY. III
- What are logical notions?
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- Eilenberg-MacLane spaces in homotopy type theory
- Constructions with Non-Recursive Higher Inductive Types
- The real projective spaces in homotopy type theory
- Higher Groups in Homotopy Type Theory
- Structuralism, Invariance, and Univalence
- Varieties of Cubical Sets
- Computational higher-dimensional type theory
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Higher Topos Theory (AM-170)
- 2-Dimensional Directed Type Theory
- Univalent categories and the Rezk completion
- An experimental library of formalized Mathematics based on the univalent foundations
- An Extension of Klein's Erlanger Program: Logic as Invariant-Theory
