The univalence axiom for elegant Reedy presheaves

DOI10.4310/HHA.2015.v17.n2.a6zbMath1352.55010arXiv1307.6248WikidataQ113999077 ScholiaQ113999077MaRDI QIDQ5963045

Michael Shulman

Publication date: 25 February 2016

Published in: Homology, Homotopy and Applications (Search for Journal in Brave)

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

zbMATH Keywords

elegant Reedy categoryhomotopy type theoryunivalence axiom

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35)

Related Items (21)

Modalities in homotopy type theory ⋮ Every Elementary Higher Topos has a Natural Number Object ⋮ Univalent completion ⋮ Constructive sheaf models of type theory ⋮ On a model invariance problem in homotopy type theory ⋮ The Interpretation Lifting Theorem for C-Systems ⋮ Two-level type theory and applications ⋮ On the ∞$\infty$‐topos semantics of homotopy type theory ⋮ What should a generic object be? ⋮ Towards a constructive simplicial model of Univalent Foundations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A type theory for synthetic $\infty$-categories ⋮ Exact completion of path categories and algebraic set theory. I: Exact completion of path categories ⋮ Unnamed Item ⋮ Univalence in locally Cartesian closed categories ⋮ Unnamed Item ⋮ The homotopy theory of type theories ⋮ Construction of the circle in \textit{UniMath} ⋮ Semantics of higher inductive types

This page was built for publication: The univalence axiom for elegant Reedy presheaves