Univalence for inverse EI diagrams (Q1689738): Difference between revisions

\textit{Homotopy type theory} [\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)] synthesizes intensional constructive type theory [\textit{P. Martin-Löf}, Intuitionistic type theory. Napoli: Bibliopolis (1984; Zbl 0571.03030)] with homotopy theory, offering the possibility of making use of type theory as a \textit{formal syntax} to prove homotopy-theoretic theorems, which would apply automatically to any homotopy theory or \(\infty\)-topos [\textit{J. Lurie}, Higher topos theory. Princeton, NJ: Princeton University Press (2009; Zbl 1175.18001); \url{https://faculty.math.illinois.edu/~rezk/homotopy-topos-sketch.pdf}]. It talks concretely about points and paths, which are then compiled by an interpretation theorem to diagrammatic arguments. This paper studies univalence providing a classifying space for all small spaces whose points are literally spaces, making available such technical tools as \textit{higher inductive types} (a formal language for cell complexes that avoids small object arguments) and Voevodsky's \textit{univalence axiom}. Higher inductive types and univalence enable \textit{synthetic homotopy theory} [\textit{D. R. Licata} and \textit{M. Shulman}, in: Proceedings of the 2013 28th annual ACM/IEEE symposium on logic in computer science, LICS 2013, Tulane University, New Orleans, LA, USA, June 25--28, 2013. Los Alamitos, CA: IEEE Computer Society. 223--232 (2013; Zbl 1369.03097); \textit{D. R. Licata} and \textit{G. Brunerie}, Lect. Notes Comput. Sci. 8307, 1--16 (2013; Zbl 1427.03033); \textit{D. R. Licata} and \textit{E. Finster}, in: Proceedings of the joint meeting of the twenty-third EACSL annual conference on computer science logic, CSL, and the 2014 29th annual ACM/IEEE symposium on logic in computer science, LICS 2014, Vienna, Austria, July 14--18, 2014. Los Alamitos, CA: IEEE Computer Society. Paper No. 66, 9 p. (2014; Zbl 1395.68249); \textit{G. Brunerie}, ``On the homotopy groups of spheres in homotopy type theory'', Preprint, \url{arXiv:1606.05916}; \textit{K.-B. Hou (Favonia)} et al., in: Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5--8, 2016. New York, NY: Association for Computing Machinery (ACM). 565--574 (2016; Zbl 1395.55011)], the last of which was the first genuinely homotopy-theoretic proof of the Blakers-Massey connectivity theorem that applies to any \(\infty\)-topos and that was finally traslated into \(\infty\)-categorical language [\url{https://faculty.math.illinois.edu/~rezk/freudenthal-and-blakers-massey.pdf}]. However, not all \(\infty\)-toposes are known to model univalence in its usual form, notably for equivariant homotopy theory. The principal objective in this paper is to generalize univalent models of [\textit{M. Shulman}, Math. Struct. Comput. Sci. 25, No. 5, 1203--1277 (2015; Zbl 1362.03008)] to include classical equivariant homotopy theory over a compact Lie group. It was shown in [\textit{A. D. Elmendorf}, Trans. Am. Math. Soc. 277, 275--284 (1983; Zbl 0521.57027)] that \(G\)-equivariant homotopy theory is equivalent to the \(\infty\)-topos of diagrams on the orbit category \(\mathcal{O}_{G}^{\mathrm{op}}\), which is an \textit{inverse EI \((\infty,1)\)-category} providing that \(G\) is a compact Lie group. Therefore, this paper aims to construct a new model category presenting the homotopy theory of presheaves on \textit{inverse EI \((\infty,1)\)-categories}, which contain universe objects abiding by Voevodsky's univalence axiom. The construction is a generalization of [\textit{M. Shulman}, Math. Struct. Comput. Sci. 25, No. 5, 1203--1277 (2015; Zbl 1362.03008)] that internalizes in an \(\left( \infty,1\right) \)-category, being an iteration of the gluing construction (i.e., comma categories) \ from [loc. cit.], where this paper generalizes by gluing along hom-functors of internal categories rather than by gluing along matching object functors. A synopsis of the paper goes as follows. \begin{itemize} \item[\S 2] recalls basic facts about indexed categories and well-founded recursion. \item[\S 3] studies \textit{internal inverse categories} in a general context to be specialized both to type theory and homotopy theory. \item[\S \S 4--6] specialize to homotopy theory, identifying diagrams on such internal categories with previously known models for \(\infty\)-toposes of diagrams. \item[\S 7] specializes to type theory, establishing that internal diagram categories admit models of homotopy type theory with univalence. \item[\S 8] addresses some examples, including equivariant homotopy theory. \end{itemize}