Univalence in locally Cartesian closed categories

DOI10.1515/forum-2015-0228zbMath1376.55018arXiv1208.1749OpenAlexW2556331506MaRDI QIDQ524707

Joachim Kock, David Gepner

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

zbMATH Keywords

univalencelocalizationinfinity-categoriesfactorization systemsinfinity-topoi

Mathematics Subject Classification ID

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