Homotopy Type Theory: Univalent Foundations of Mathematics

zbMath1298.03002arXiv1308.0729MaRDI QIDQ5420262

Unnamed Author

Publication date: 11 June 2014

Full work available at URL: https://arxiv.org/abs/1308.0729

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Categorical logic, topoi (03G30) Research exposition (monographs, survey articles) pertaining to algebraic topology (55-02) Categories of sets, characterizations (18B05) Topological categories, foundations of homotopy theory (55U40) Foundations, relations to logic and deductive systems (18A15)

Related Items

On representations of intended structures in foundational theories, Categorical structures for type theory in univalent foundations, The future of mathematics in economics: a philosophically grounded proposal, Left-exact localizations of \(\infty\)-topoi. I: Higher sheaves, Formalizing mathematical knowledge as a biform theory graph: a case study, Category theory, logic and formal linguistics: some connections, old and new, Canonicity of weak \(\omega\)-groupoid laws using parametricity theory, From reversible programs to univalent universes and back, Finitary higher inductive types in the groupoid model, A characterisation of elementary fibrations, A constructive manifestation of the Kleene-Kreisel continuous functionals, The intrinsic topology of Martin-Löf universes, The construction of set-truncated higher inductive types, General proof theory: introduction, Aligning concepts across proof assistant libraries, Game semantics for dependent types, Decomposition spaces, incidence algebras and Möbius inversion. I: Basic theory, Computational logic: its origins and applications, Univalent completion, Algorithmic Theories of Problems. A Constructive and a Non-Constructive Approach, Homotopy type theory and Voevodsky’s univalent foundations, Foundations of dependent interoperability, Internal languages of finitely complete \((\infty , 1)\)-categories, Observability in the univalent universe, Homotopy type theory in Lean, Constructive knowledge and the justified true belief paradigm, To be or not to be constructive, that is not the question, An implementation of effective homotopy of fibrations, The Local Universes Model, Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda, Proof Assistants for Natural Language Semantics, Identity and intensionality in univalent foundations and philosophy, Klein-Weyl's program and the ontology of gauge and quantum systems, Homotopical inverse diagrams in categories with attributes, Carnap and the invariance of logical truth, Type-theoretic approaches to ordinals, Towards a homotopy domain theory, Graph theory in Coq: minors, treewidth, and isomorphisms, Polynomial functors and combinatorial Dyson–Schwinger equations, What inductive explanations could not be, Denotational semantics of recursive types in synthetic guarded domain theory, The categorical imperative: category theory as a foundation for deontic logic, A type theory for synthetic $\infty$-categories, True V or Not True V, That Is the Question, Displayed Categories, Effective Validity: A Generalized Logic for Stable Approximate Inference, Composition of deductions within the propositions-as-types paradigm, Bousfield localisation and colocalisation of one-dimensional model structures, Classical misuse attacks on NIST round 2 PQC. The power of rank-based schemes, Characterizations of modalities and lex modalities, The Cantor-Schröder-Bernstein theorem for \(\infty\)-groupoids, Constructing a universe for the setoid model, Mathesis Universalis and Homotopy Type Theory, From Mathesis Universalis to Provability, Computability, and Constructivity, On abstraction in mathematics and indefiniteness in quantum mechanics, Brouwer's fixed-point theorem in real-cohesive homotopy type theory, Validating Brouwer's continuity principle for numbers using named exceptions, The category of equilogical spaces and the effective topos as homotopical quotients, Fibrational modal type theory, New perspectives on the hole argument, The hole argument in homotopy type theory, The hole argument, take \(n\), Univalent polymorphism, Unnamed Item, Univalence in locally Cartesian closed categories, A dependent type theory with abstractable names, Combinatorial structure of type dependency, Cubical Type Theory: a constructive interpretation of the univalence axiom, Foreword to the special focus on formal proofs for mathematics and computer science, The homotopy theory of type theories, Univalence as a principle of logic, Combinatorial topology and constructive mathematics, Construction of the circle in \textit{UniMath}, The simplicial model of univalent foundations (after Voevodsky), A constructive approach to Freyd categories, The justification of identity elimination in Martin-Löf's type theory, Filter quotients and non-presentable \((\infty,1)\)-toposes, Isomorphism is equality, A meaning explanation for HoTT, Exercising Nuprl’s Open-Endedness, Preface: Special issue on homotopy type theory and univalent foundations, Canonicity for cubical type theory, Guarded cubical type theory, The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory, From signatures to monads in \textsf{UniMath}, Categoricity results and large model constructions for second-order ZF in dependent type theory, Unnamed Item, Unnamed Item, Towards a Cubical Type Theory without an Interval, Heterogeneous Substitution Systems Revisited, The structuralist mathematical style: Bourbaki as a case study, Predicativity and constructive mathematics, Automorphisms of types in certain type theories and representation of finite groups, A homotopy-theoretic model of function extensionality in the effective topos, First steps towards a formalization of forcing, Natural models of homotopy type theory, On endotrivial modules for Lie superalgebras, Rensets and renaming-based recursion for syntax with bindings, Univalence and completeness of Segal objects, Constructive mathematics, Church's thesis, and free choice sequences, LF+ in Coq for "fast and loose" reasoning, Modalities in homotopy type theory, From type theory to setoids and back, Localization in Homotopy Type Theory, AFFINE LOGIC FOR CONSTRUCTIVE MATHEMATICS, Unnamed Item, Homotopical patch theory, Proof-relevance in Bishop-style constructive mathematics, Cubical methods in homotopy type theory and univalent foundations, On Church’s thesis in cubical assemblies, Naive cubical type theory, Bicategories in univalent foundations, The Scott model of PCF in univalent type theory, Synthetic topology in Homotopy Type Theory for probabilistic programming, Partiality and Container Monads, Axiomatic Thinking, Identity of Proofs and the Quest for an Intensional Proof-Theoretic Semantics, Hom weak ω-categories of a weak ω-category, Unnamed Item, Every Elementary Higher Topos has a Natural Number Object, Direct spectra of Bishop spaces and their limits, Martin Hofmann’s contributions to type theory: Groupoids and univalence, Elementary fibrations of enriched groupoids, Constructive sheaf models of type theory, Unnamed Item, Unnamed Item, Higher-order games with dependent types, Higher Structures in M‐Theory, The Rational Higher Structure of M‐theory, Unnamed Item, Unnamed Item, Eilenberg-MacLane spaces and stabilisation in homotopy type theory, Univalent Foundations and the Equivalence Principle, Higher Structures in Homotopy Type Theory, Univalent Foundations and the UniMath Library, Models of HoTT and the Constructive View of Theories, Set Theory and Structures, A New Foundational Crisis in Mathematics, Is It Really Happening?, A Comparison of Type Theory with Set Theory, What Do We Want a Foundation to Do?, A class of higher inductive types in Zermelo‐Fraenkel set theory, Homotopy composition of cospans, Subtyping without reduction, Calculating datastructures, Rensets and renaming-based recursion for syntax with bindings extended version, The Hurewicz theorem in homotopy type theory, Representation and Spacetime: The Hole Argument Revisited, The Interpretation Lifting Theorem for C-Systems, Canonicity and homotopy canonicity for cubical type theory, Leibniz equality is isomorphic to Martin-Löf identity, parametrically, Five stages of accepting constructive mathematics, The calculus of dependent lambda eliminations, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Reversible monadic computing, Unnamed Item, Unnamed Item, A Homological Theory of Functions: Nonuniform Boolean Complexity Separation and VC Dimension Bound Via Algebraic Topology, and a Homological Farkas Lemma, A Syntax for Higher Inductive-Inductive Types, Nilpotent types and fracture squares in homotopy type theory, Ornaments for Proof Reuse in Coq, EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS, Indexed type theories, Extensional constructive real analysis via locators, Injective types in univalent mathematics, Homotopy type-theoretic interpretations of constructive set theories, For Finitary Induction-Induction, Induction is Enough, Is Impredicativity Implicitly Implicit, Good Fibrations through the Modal Prism, Introduction – from type theory and homotopy theory to univalent foundations, Displayed Categories, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, An introduction to univalent foundations for mathematicians, Unnamed Item, FROM MULTISETS TO SETS IN HOMOTOPY TYPE THEORY, Multisets in type theory, Semantics of higher inductive types, Unnamed Item, Proof Theory of Constructive Systems: Inductive Types and Univalence, Cartesian cubical computational type theory: Constructive reasoning with paths and equalities, Constructive Galois Connections, W-types in setoids, Unnamed Item, UNIVERSES AND UNIVALENCE IN HOMOTOPY TYPE THEORY, Models of Type Theory Based on Moore Paths, Unnamed Item, Unnamed Item, Cubical Agda: A dependently typed programming language with univalence and higher inductive types, Extensional equality preservation and verified generic programming, Modal descent, Syntax and models of Cartesian cubical type theory, CATEGORICAL HARMONY AND PATH INDUCTION, A rewriting coherence theorem with applications in homotopy type theory, The compatibility of the minimalist foundation with homotopy type theory, Strange new universes: Proof assistants and synthetic foundations, On Small Types in Univalent Foundations, Univalent categories of modules, A general framework for the semantics of type theory, On notions of compactness, object classifiers, and weak Tarski universes, The long exact sequence of homotopy n-groups, Two-level type theory and applications, Monoidal weak ω-categories as models of a type theory, On the ∞$\infty$‐topos semantics of homotopy type theory, Formalising basic topology for computational logic in simple type theory, An intuitionistic set-theoretical model of fully dependent CC, What should a generic object be?, Yoneda lemma for simplicial spaces, Towards a constructive simplicial model of Univalent Foundations, A groupoid approach to regular \(\ast \)-semigroups, Game semantics of Martin-Löf type theory, Unnamed Item, Unnamed Item