Univalence in locally Cartesian closed categories
From MaRDI portal
Publication:524707
DOI10.1515/forum-2015-0228zbMath1376.55018arXiv1208.1749OpenAlexW2556331506MaRDI QIDQ524707
Publication date: 3 May 2017
Published in: Forum Mathematicum (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1208.1749
Abstract and axiomatic homotopy theory in algebraic topology (55U35) Categorical semantics of formal languages (18C50)
Related Items (19)
Modalities in homotopy type theory ⋮ Graphs, hypergraphs, and properads ⋮ THE TOM DIECK SPLITTING THEOREM IN EQUIVARIANT MOTIVIC HOMOTOPY THEORY ⋮ Model topoi and motivic homotopy theory ⋮ $L'$-localization in an $\infty$-topos ⋮ Data Types with Symmetries and Polynomial Functors over Groupoids ⋮ Every Elementary Higher Topos has a Natural Number Object ⋮ Univalent completion ⋮ CONDITIONAL FLATNESS, FIBERWISE LOCALIZATIONS, AND ADMISSIBLE REFLECTIONS ⋮ Polynomial functors and combinatorial Dyson–Schwinger equations ⋮ Brouwer's fixed-point theorem in real-cohesive homotopy type theory ⋮ Indexed type theories ⋮ Exact completion of path categories and algebraic set theory. I: Exact completion of path categories ⋮ Parametrized spectra, multiplicative Thom spectra and the twisted Umkehr map ⋮ The \(\infty\)-categorical Eckmann-Hilton argument ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ Semantics of higher inductive types ⋮ Filter quotients and non-presentable \((\infty,1)\)-toposes ⋮ The effective model structure and -groupoid objects
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
- Motivic twisted \(K\)-theory
- Mini-workshop: The homotopy interpretation of constructive type theory. Abstracts from the mini-workshop held February 27th-March 05th, 2011.
- Mapping spaces in quasi-categories
- Grothendieck quasitoposes
- The identity type weak factorisation system
- Sheaves in geometry and logic: a first introduction to topos theory
- On localization and stabilization for factorization systems
- Théories homotopiques dans les topos. (Homotopy theories in topoi)
- Quasi-categories and Kan complexes
- The simplicial model of univalent foundations (after Voevodsky)
- Enriched \(\infty\)-categories via non-symmetric \(\infty\)-operads
- Weak omega-categories from intensional type theory
- The Local Universes Model
- Homotopy-Theoretic Models of Type Theory
- Types are weak ω -groupoids
- Univalent Semantics of Constructive Type Theories
- Homotopy theoretic models of identity types
- A model for the homotopy theory of homotopy theory
- The law of excluded middle in the simplicial model of type theory
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Higher Topos Theory (AM-170)
- Univalence for inverse diagrams and homotopy canonicity
- \(\mathbb{A}^1\)-homotopy theory of schemes
- The univalence axiom for elegant Reedy presheaves
This page was built for publication: Univalence in locally Cartesian closed categories
