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.

Review text

A Kan fibration \(p\) of simplicial sets is called \textit{universal} if every fibration satisfying a certain set-theoretic size restriction (typically on the cardinality of the fibre) is a homotopy pullback of \(p\). The fibration \(p\) is called \textit{univalent} if, roughly speaking, the path space of the base of \(p\) is weakly equivalent to the space of (parametrised) weak equivalences between fibres of \(p\). In the paper under review, the authors prove in Theorem 2 that for any fibration \(E \rightarrow B\) there exists a univalent fibration \(E' \rightarrow B'\) (in the same set-theoretic universe) with \(B \subseteq B'\), together with a map of fibrations resulting in a homotopy pullback square (so that the map \(E \rightarrow B \times_{B'} E'\) is a weak equivalence): \[ \begin{matrix} E & \rightarrow & E' \\ \downarrow && \downarrow \\ B & \subseteq & B' \end{matrix} \] Moreover, if \(p\) is universal then \(p'\) is universal as well. The paper uses the machinery of actions of simplicial groupoids on simplicial sets, developed in \S\S2--3. Universality and univalence are discussed in \S4, and \S5 is devoted to the formulation and proof of Theorem 2. The paper requires no background in type theory. It is carefully written and self-contained, assuming only familiarity with basic homotopy theory of simplicial sets.

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)