Univalent categories and the Rezk completion

DOI10.1017/S0960129514000486zbMath1362.18003DBLPjournals/mscs/AhrensKS15arXiv1303.0584WikidataQ59757167 ScholiaQ59757167MaRDI QIDQ5740648

Krzysztof Kapulkin, Michael Shulman, Benedikt Ahrens

Publication date: 27 July 2016

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Foundations, relations to logic and deductive systems (18A15)

Related Items (23)

Categorical structures for type theory in univalent foundations ⋮ The construction of set-truncated higher inductive types ⋮ Bicategories in univalent foundations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Homotopy type theory in Lean ⋮ Univalent Foundations and the Equivalence Principle ⋮ Higher Structures in Homotopy Type Theory ⋮ Bicategorical type theory: semantics and syntax ⋮ Unnamed Item ⋮ Univalent foundations as structuralist foundations ⋮ Unnamed Item ⋮ A type theory for synthetic $\infty$-categories ⋮ Displayed Categories ⋮ Displayed Categories ⋮ Unnamed Item ⋮ An introduction to univalent foundations for mathematicians ⋮ Isomorphism is equality ⋮ Axiomatizations of arithmetic and the first-order/second-order divide ⋮ Some Wellfounded Trees in UniMath ⋮ From signatures to monads in \textsf{UniMath} ⋮ Heterogeneous Substitution Systems Revisited ⋮ Univalence and completeness of Segal objects

Cites Work

• Isomorphism is equality
• A model for the homotopy theory of homotopy theory
• A Machine-Checked Proof of the Odd Order Theorem

This page was built for publication: Univalent categories and the Rezk completion