Univalent completion

DOI10.1007/S00208-017-1614-3MaRDI QIDQ1659918zbMATH OpenOpenAlexWikidataFDO

Authors Benno van den Berg, Ieke Moerdijk

Publication date 23 August 2018

Published in Mathematische Annalen (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

groupoid actionhomotopy pullbacksimplicial groupoidunivalent fibrationuniversal fibration

Mathematics Subject Classification ID

Categorical semantics of formal languages (18C50) Classification of fiber spaces or bundles in algebraic topology (55R15) Simplicial sets and complexes in algebraic topology (55U10)

Abstract: We review the concept of a univalent fibration and show by elementary means that every Kan fibration in simplicial sets can be embedded in a univalent Kan fibration.

Recommendations

• The simplicial model of univalent foundations (after Voevodsky)
• Fibrations of simplicial sets
• Effective Kan fibrations in simplicial sets
• Univalence and completeness of Segal objects
• Univalence for inverse diagrams and homotopy canonicity

Cites work

• Finite sets and symmetric simplicial sets
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 4163134 (Why is no real title available?)
• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• scientific article; zbMATH DE number 3264757 (Why is no real title available?)
• scientific article; zbMATH DE number 3297895 (Why is no real title available?)
• The homotopy theory of type theories
• The univalence axiom for elegant Reedy presheaves
• Univalence for inverse diagrams and homotopy canonicity
• Univalence in locally Cartesian closed categories
• W-types in homotopy type theory

Cited in

(6)

• A unified functional look at completion in MET, UNIF and AP
• Univalence and completeness of Segal objects
• Uniform ideal completions
• The effective model structure and \(\infty\)-groupoid objects
• The category of -finite spaces
• (, 1)-categorical comprehension schemes

This page was built for publication: Univalent completion

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1659918)