The simplicial model of univalent foundations (after Voevodsky)
From MaRDI portal
Publication:2031691
DOI10.4171/JEMS/1050zbMath1471.18025arXiv1211.2851MaRDI QIDQ2031691
Krzysztof Kapulkin, Peter LeFanu Lumsdaine
Publication date: 10 June 2021
Published in: Journal of the European Mathematical Society (JEMS) (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1211.2851
Simplicial sets and complexes in algebraic topology (55U10) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Categorical semantics of formal languages (18C50) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)
Related Items
Modalities in homotopy type theory, A characterisation of elementary fibrations, Towards a directed homotopy type theory, The construction of set-truncated higher inductive types, Cubical methods in homotopy type theory and univalent foundations, Bicategories in univalent foundations, Observability in the univalent universe, Homotopy type theory in Lean, Naïve Type Theory, Univalent Foundations and the Equivalence Principle, A New Foundational Crisis in Mathematics, Is It Really Happening?, The Hurewicz theorem in homotopy type theory, Strange new universes: Proof assistants and synthetic foundations, The Interpretation Lifting Theorem for C-Systems, On Small Types in Univalent Foundations, Univalent categories of modules, Bicategorical type theory: semantics and syntax, On the ∞$\infty$‐topos semantics of homotopy type theory, Canonicity and homotopy canonicity for cubical type theory, What should a generic object be?, Towards a constructive simplicial model of Univalent Foundations, C-system of a module over a \(Jf\)-relative monad, Unnamed Item, Unnamed Item, Unnamed Item, A type theory for synthetic $\infty$-categories, Unnamed Item, Univalence in locally Cartesian closed categories, The Frobenius condition, right properness, and uniform fibrations, Unnamed Item, Filter quotients and non-presentable \((\infty,1)\)-toposes, Guarded cubical type theory, From signatures to monads in \textsf{UniMath}, Models of Type Theory Based on Moore Paths, Cubical Agda: A dependently typed programming language with univalence and higher inductive types, The effective model structure and -groupoid objects, Model structure on the universe of all types in interval type theory, Syntax and models of Cartesian cubical type theory
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Univalence in locally Cartesian closed categories
- The identity type weak factorisation system
- On the strength of dependent products in the type theory of Martin-Löf
- Generalized algebraic theories and contextual categories
- Comprehension categories and the semantics of type dependency
- Wellfounded trees in categories
- Homotopy type theory and Voevodsky’s univalent foundations
- Products of families of types and (Pi,lambda)-structures on C-systems
- The Local Universes Model
- The (Pi,lambda)-structures on the C-systems defined by universe categories
- Subsystems and regular quotients of C-systems
- A Survey of Graphical Languages for Monoidal Categories
- Homotopy-Theoretic Models of Type Theory
- Types are weak ω -groupoids
- Locally cartesian closed categories and type theory
- A C-system defined by a universe category
- Homotopy theoretic models of identity types
- Internal type theory
- Circuits as streams in Coq: Verification of a sequential multiplier
- An introduction to univalent foundations for mathematicians
- A category-theoretic account of program modules
- On Semisimplicial Fibre-Bundles
- Homotopy Type Theory: Univalent Foundations of Mathematics
- The Geometric Realization of a Kan Fibration is a Serre Fibration
- Types for Proofs and Programs
- W-types in homotopy type theory
- Univalence for inverse diagrams and homotopy canonicity
- An experimental library of formalized Mathematics based on the univalent foundations
