Effective Kan fibrations in simplicial sets (Q2094622)

This book redevelops the foundations of simplicial homotopy theory, in particular around the Kan-Quillen model structure on simplicial sets in a more effective or structured style. The authors' motivation comes from homotopy type theory (HoTT) [\textit{The Univalent Foundations Program}, Homotopy type theory. Univalent foundations of mathematics. Princeton, NJ: Institute for Advanced Study; Raleigh, NC: Lulu Press (2013; Zbl 1298.03002)] and Voevodsky's construction of a model of HoTT in simplicial sets [\textit{K. Kapulkin} and \textit{P. L. Lumsdaine}, J. Eur. Math. Soc. (JEMS) 23, No. 6, 2071--2126 (2021; Zbl 1471.18025)]. The main constribution of the book is the introduction of the notion of an \textit{effective Kan fibration}, structured notion of Kan fibration. One fundamental obstacle with building Voevodsky's model in simplicial sets \textit{constructively} was identified by \textit{M. Bezem} et al. [LIPIcs -- Leibniz Int. Proc. Inform. 38, 92--106 (2015; Zbl 1433.03154)]. To interpret \(\Pi\)-types in simplicial sets, one should appeal to the fact that the pullback functor along any map has a right adjoint called \textit{pushforward}. Since the type families are interpreted as Kan fibrations in Voevodsky's model, one has to show that Kan fibrations are closed under pushforward along Kan fibrations, which is valid classically while it was shown in [\textit{M. Bezem} et al., LIPIcs -- Leibniz Int. Proc. Inform. 38, 92--106 (2015; Zbl 1433.03154)] that the result is constructively improvable (\textit{BCP-obstruction}). \textit{N. Gambino} and \textit{C. Sattler} [J. Pure Appl. Algebra 221, No. 12, 3027--3068 (2017; Zbl 1378.18002)] defined a structured notion of a \textit{uniform Kan fibration}, establishing constructively that uniform Kan fibrations are closed under pushforward. It was then shown that their definition is classically correct in the sense that a map can be rigged out in the structure of a uniform Kan fibration iff it has the right lifting property against the horn inclusions. Gambino and Sattler ran into trouble with universes as another type constructor. The only known method for constructing universal fibrations in presheaf categories is via the Hofmann-Streicher construction [\url{https://www2.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf}], which can only be applied to the notions of fibered structure which are local. Effective Kan fibrations have the advantage of being local, while uniform Kan fibrations are not local. The synoposis of the book goes as follows. \begin{itemize} \item[Chapter 1] is an introduction. \end{itemize} Part I: This part aims to derive the existence of \(\Pi\)-types in an axiomatic setting based on a suitable combination of a dominance and a symmetric Moore structure. \begin{itemize} \item[Chapter 2] studies new notions of \textit{fibered structure} and \textit{cofibered structure} on a category \(\mathcal{E}\). \item[Chapter 3] shows how the notion of a \textit{dominance} gives rise to an algebraic weak factorization in which the left class is shown to be the class of \textit{effective cofibrations} while the right class is called the class of \textit{effective trivial fibrations}. The double category of effective cofibrationns is investigated a bit more closely. \item[Chapter 4] constructs an algebraic weak factorization system on a \textit{category with Moore structure} \(\mathcal{E}\), studying its coalgebras and algebras more closely. It is shown that the structure of a coalgebra is equivalent to the structure of \textit{hyperdeformation retract} (HDR), while algebras are identified as \textit{naive fibrations}. \item[Chapter 5] aims to establish a Frobenius property for the AWFS constructed in the previous chapter in the case that the Moore structure comes equipped with a certain additional symmetry. \item[Chapter 6] connects the two algebraic weak factorization systems coming from a dominance and a Moore structure to define the notion of \textit{effective fibration}. \item[Chapter 7] gives the main result of the first part, which provides a constructive proof of the fact when \(X\)\ is effectively fibrant and \(A\)\ is any other object, then the exponential \(X^{A}\)\ is effectively fibrant. \end{itemize} Part II: This part is devoted to one particular example, namely, simplicial sets. \begin{itemize} \item[Chapter 8] chooses a suitable dominance in simplicial sets. The main results are that being an effective trivial Kan fibration is a local notion of fibered structure, and that in a classical metatheory, a map can be equipped with structure of an effective trivial Kan fibration iff it has the right lifting property against boundary inclusions. \item[Chapter 9] aims to show that the category of simplicial sets is to be equipped with symmetric Moore structure. \item[Chapter 10] aims to take a closer look at the AWFS with the coalgebras for the comonad being called the \textit{HDRs} and the algebras for the monad being called the \textit{naive Kan fibrations}. \item[Chapter 11] studies effective Kan fibrations in simplicial sets, aiming to show that there is a small triple category of mould squares against which effective Kan fibrations are those maps having the right lifting property. \item[Chapter 12] aims to show that the notion of an effective Kan fibration in simplicial sets is both local and classically correct. \item[Chapter 13] takes stock of the properties of effective Kan fibrations established so far, outlining some directions for future research. \end{itemize} Appendices: \begin{itemize} \item[Appendix A] collects the axioms for a Moore category and a dominance. \item[Appendix B] shows that the category of cubical sets can be rigged out in parts of the definition of a Moore structure. \item[Appendix C] aims to show that horn lifting problems have at most one degenerate filler. \item[Appendix D] is devoted to a proof showing that the notion of a uniform Kan fibration is not a local notion of fibered structure. \end{itemize}