\documentclass[11pt,letterpaper]{article} \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} \usepackage{lmodern} \usepackage[margin=1.05in]{geometry} \usepackage{microtype} \usepackage{amsmath,amssymb,amsthm,mathtools} \usepackage{enumitem,booktabs,longtable} \usepackage{xcolor} \definecolor{paperlink}{RGB}{0,0,114} \usepackage{hyperref} \hypersetup{colorlinks=true,linktoc=all,linkcolor=paperlink,citecolor=paperlink,urlcolor=paperlink,pdfstartview=Fit,pdftitle={Higher Galois Recognition and Parameter Descent},pdfauthor={Zhenyu Sun}} \pagestyle{plain} \setlength{\parindent}{1.25em} \setlength{\parskip}{0pt} \setlist{itemsep=3pt,topsep=5pt} \setlist[enumerate,1]{label=\textup{(\roman*)}} \setlength{\emergencystretch}{2em} \numberwithin{equation}{section} \newtheorem{theorem}{Theorem}[section] \newtheorem{proposition}[theorem]{Proposition} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \newtheorem{example}[theorem]{Example} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \newcommand{\Sps}{\mathcal S} \newcommand{\Spi}{\mathcal S_\pi} \newcommand{\Fn}{\mathcal F_n} \newcommand{\C}{\mathcal C} \newcommand{\D}{\mathcal D} \newcommand{\X}{\mathcal X} \newcommand{\Y}{\mathcal Y} \newcommand{\Z}{\mathcal Z} \newcommand{\M}{\mathcal M} \newcommand{\coh}{\mathrm{coh}} \newcommand{\op}{\mathrm{op}} \newcommand{\id}{\mathrm{id}} \DeclareMathOperator{\Map}{Map} \DeclareMathOperator{\Fun}{Fun} \DeclareMathOperator{\Nat}{Nat} \DeclareMathOperator{\Aut}{Aut} \DeclareMathOperator{\Hom}{Hom} \DeclareMathOperator{\Tot}{Tot} \DeclareMathOperator{\Mod}{Mod} \DeclareMathOperator{\Sec}{Sec} \DeclareMathOperator{\sk}{sk} \DeclareMathOperator{\cosk}{cosk} \DeclareMathOperator{\im}{im} \DeclareMathOperator{\coker}{coker} \DeclareMathOperator*{\colim}{colim} \title{Higher Galois Recognition and Parameter Descent\\[5pt] \large Model groupoids and finite homotopy semantics, II} \author{Zhenyu Sun} \date{} \begin{document} \maketitle \begin{abstract} Let $n\geq0$ and let $\mathcal X$ be a bounded coherent $\infty$-topos. Suppose that finitely many noninitial coherent $n$-truncated objects cover its terminal object, and that every coherent $n$-truncated object in each of their slices has a finite covering family of sections. We identify $\mathcal X^{\coh}_{\leq n}$ with $\Fun(M,\mathcal S_{\pi,\leq n})$ for a $\pi$-finite $(n+1)$-type $M$, recovered by all finite models preserving finite limits, finite coproducts, and effective epimorphisms. Descent uses degrees through $n+2$ for objects and $n+1$ for maps; both bounds are sharp for finite homotopy actions. Every exact functor $F$ between recognized categories has a universal parameter $P_F=F_!(1)$ and a canonical factorization through its slice with fully faithful second functor. This parameter characterizes full faithfulness, conservativity, and all exact slice factorizations. For successive abelian Postnikov layers, we identify the space of marked exact lifts with a path space of Eilenberg--Mac Lane sections with local coefficients. The obstruction, classes of lifts, and relative automorphisms occur in degrees $r+1$, $r$, and $r-1$. We compute a twisted parity obstruction and, for odd primes, classify cyclic self-equivalence components by a $p$-adic valuation. A nonzero Postnikov class can persist in the identity component. For continuous finite families over a profinite $(n+1)$-type, we prove that a uniform finite-section atlas exists precisely when the complete model space is $\pi$-finite. Exact functors from finite model semantics, together with their lift spaces, satisfy finite-stage descent, while explicit profinite examples separate objectwise trivialization from uniform parameter elimination. \end{abstract} \setcounter{tocdepth}{1} \begingroup \small \makeatletter \renewcommand{\l@section}{\@dottedtocline{1}{0em}{1.8em}} \makeatother \tableofcontents \endgroup \clearpage \section{Introduction} Finite homotopy semantics retains finite parameter spaces together with homotopies between their maps. Its recognition problem has a relative form: after identifying a category of finite families, one must determine which exact functors descend without parameters, which acquire a fully faithful factorization after adjoining a parameter, and which lift through the next homotopy layer. The answers involve a universal parameter object, relative Postnikov classes, and the monodromy of the space of lifts. This is the second paper in a series on model groupoids and finite homotopy semantics. The first studies definability after restriction to a model subgroupoid and the extension of finite group actions~\cite{SunDefinabilityLifting}. Here the relative problem also retains higher transformations and successive Postnikov layers. The definitions and proofs needed below are given independently. Fix $n\geq0$ and write $\Fn=\mathcal S_{\pi,\leq n}$ for the $\infty$-category of $\pi$-finite $n$-types. Its mapping spaces are $n$-truncated, while its core is an $(n+1)$-type. Accordingly, finite $n$-type semantics detects an $(n+1)$-type of models. For a space $M$, put \[ \mathcal L_n(M)=\Fun(M,\Fn). \] Throughout, an \emph{exact functor} preserves finite limits, finite coproducts, and effective epimorphisms. Exact functor categories include all natural transformations and higher homotopies. \subsection{Recognition and bounded descent} Our categorical input is a bounded coherent $\infty$-topos $\X$ and $\C=\X^{\coh}_{\leq n}$. A finite local-section atlas is an effective epimorphism \[ \coprod_{i\in I}P_i\longrightarrow1 \] with finitely many noninitial $P_i\in\C$, such that every object of $\C/P_i$ has an effective epimorphism from a finite coproduct of the terminal object of that slice. This is a condition inside $\C$ on its objects, sections, and covering maps. Theorems~\ref{hr:thm-atlas} and~\ref{hr:thm-models}, together with Proposition~\ref{hc:prop-converse}, prove that this condition is equivalent to \begin{equation}\label{eq:intro-recognition} \C\simeq\mathcal L_n(M) \end{equation} for a $\pi$-finite $(n+1)$-type $M$. The full category of exact models $\C\to\Fn$ is precisely $M$. The atlas objects represent the fibre functors, and Yoneda supplies all their transformations: \begin{equation}\label{eq:intro-model-maps} \Nat\bigl(\Map_\C(P_i,-),\Map_\C(P_j,-)\bigr) \simeq\Map_\C(P_j,P_i). \end{equation} Every arrow between atlas objects is proved to be an equivalence. Their opposite groupoid therefore reconstructs $M$, independently of the atlas. The proof first derives full faithfulness of constants from finite covering families of sections. An induction on truncation degree then reconstructs every local object from points and their path objects. Effective descent assembles the slices. For a degreewise finite Kan presentation $G_\bullet$ of $M$, the resulting formula is \begin{equation}\label{eq:intro-finite} \C\simeq \lim_{[q]\in\Delta_{\leq n+2}}\Fn^{G_q}. \end{equation} Maps between objects carrying descent data require only degrees through $n+1$. Both bounds are optimal within the descent diagrams of finite $C_2$-actions (Proposition~\ref{hs:prop-sharp-actions}). The comparison criterion in Section~\ref{sec:comparison} also applies when a point atlas has not been given. \subsection{Universal parameters of exact functors} Let $F:\C\to\D$ be exact between categories recognized at the same level. Theorem~\ref{thm:universal-parameter} constructs a left adjoint $F_!$ and the intrinsic object \[ P_F=F_!(1_\D). \] For every $A\in\C$, its universal property is \begin{equation}\label{eq:intro-universal-parameter} \Map_\C(P_F,A)\simeq\Map_\D(1_\D,F(A)). \end{equation} This space also classifies exact factorizations of $F$ through $\C/A$, including the chosen identification of their composite with $F$. The distinguished section of $F(P_F)$ gives a canonical factorization \begin{equation}\label{eq:intro-parameter-factor} \C\longrightarrow\C/P_F\longrightarrow\D \end{equation} whose second functor is fully faithful. It is the unique such slice factorization, up to contractible choice. The object $P_F$ tests two different properties: \[ \begin{aligned} F\text{ is fully faithful} &\quad\Longleftrightarrow\quad P_F\simeq1_\C,\\ F\text{ is conservative} &\quad\Longleftrightarrow\quad P_F\to1_\C \text{ is an effective epimorphism}. \end{aligned} \] In the second case, the powers of this same intrinsic parameter give the finite descent formula with the sharp cutoffs $n+2$ and $n+1$. For $F=f^*$, its fibre at $x$ is $\tau_{\leq n}\operatorname{hofib}_x(f)$. Thus the construction is an internal form of relative truncation, together with a classification of all possible exact parameter extensions. Composition and change of parameters satisfy \[ P_{GF}\simeq F_!P_G, \qquad P_{F_A}\simeq(A\times P_F\to A). \] \subsection{Lifting through successive homotopy layers} Let $r\geq2$, and let $X,Y$ be $\pi$-finite $r$-types. Write $B_X=\tau_{\leq r-1}X$, $B_Y=\tau_{\leq r-1}Y$, and let $A_X,A_Y$ be their top local coefficient systems. A lower exact functor is a map $f:B_Y\to B_X$. Prescribe also a homomorphism $\alpha:A_Y\to f^*A_X$. If $\kappa_X,\kappa_Y$ are the Postnikov classes, Theorem~\ref{thm:relative-postnikov-lifts} identifies the complete space of marked exact lifts with a path space between their classifying sections. In particular, the obstruction is \begin{equation}\label{eq:intro-postnikov-obstruction} f^*\kappa_X-\alpha_*\kappa_Y \in H^{r+1}(B_Y;f^*A_X). \end{equation} When it vanishes, the lift space is a torsor for the section space $\Gamma_{B_Y}K_{B_Y}(f^*A_X,r)$. Its components form an $H^r$-torsor, and its $i$th homotopy group is $H^{r-i}$ for $1\leq i\leq r$. The lower functor and its band map determine whether these lifts are fully faithful or invertible. The functor moduli are recovered by retaining transport in the space of lower data. In the cyclic examples of Section~\ref{sec:cyclic-lifting}, existence is an explicit scalar equation, and forgetting a lower marking produces a computable translation action. A separate example with the sign action on $\mathbb Z/4$ exhibits a parity obstruction: a fixed lower identity admits a fully faithful next-level lift precisely in the odd degrees (Proposition~\ref{prop:twisted-postnikov-parity}). The higher gauge calculation classifies cyclic self-equivalence components in every degree. For $r=2j-1$, their full homotopy type depends on the $p$-adic valuation of $j$ (Corollary~\ref{cor:cyclic-padic-component}). It distinguishes fundamental groups $C_{p^2}$ and $C_p\times C_p$, and in degree $2p-1$ retains the original nonzero Postnikov class inside the identity component of the self-equivalence space (Example~\ref{ex:cyclic-gauge-frobenius}). \subsection{The finite boundary inside continuous semantics} For a profinite $(n+1)$-type $P=\{P_i\}$, define \[ \mathcal C_n(P)=\colim_i\mathcal L_n(P_i). \] These are continuous finite families. Higher Stone duality gives full duality with exact functors in this fixed range, and \[ \Mod_n(\mathcal C_n(P))\simeq\lim_iP_i. \] Theorem~\ref{pf:thm-uniform} proves an exact criterion for the uniformity of parameters: $\mathcal C_n(P)$ has a finite local-section atlas if and only if this whole model space is $\pi$-finite, equivalently if and only if $P$ is represented by a single $\pi$-finite $(n+1)$-type. Every prescribed finite family still becomes constant on some finite coherent cover. Finite continuous $\mathbb Z_p$-sets show why these separate covers need not yield a common atlas. \subsection{Relation to existing theory} The identification of fibre-functor endomorphisms with loop spaces belongs to higher Galois theory; see To\"en~\cite{ToenGalois} and Hoyois~\cite{HoyoisHigherGalois}. The coherent and Stone frameworks are developed in Exodromy~\cite{BGHExodromy}, and the finite homotopy closure properties used here are treated by Anel~\cite{AnelPiFinite}. The finite totalization cutoffs follow from standard truncation arguments~\cite{AnelPiFinite,HesselholtPstragowskiDirac}. The relative obstruction calculation uses the classical classification of Eilenberg--Mac Lane fibrations and their section spaces~\cite{MollerSections,MollerSchererPostnikov}. The results below organize these constructions around an intrinsic finite-section condition. They derive its full model space, identify the universal parameter of every exact functor, and translate successive Postnikov compatibility into the full moduli of exact lifts. The explicit action examples establish the sharp descent bounds and calculate the distinction between marked and unmarked lifts. The uniform parameter theorem then identifies precisely when continuous semantics reduces to the finite recognition statement. All recognition statements concern a prescribed truncation range. The local-section hypothesis quantifies over all coherent objects in that range. A finite simplicial window bounds the coherence data used for a given valid presentation; its underlying homotopy type is $\pi$-finite and can have nonzero cohomology in arbitrarily high degrees. \section{Finite homotopy semantics and effective quotients} \label{sec:foundations} All categories, limits, colimits, and mapping spaces are interpreted in the $\infty$-categorical sense unless stated otherwise. A space is $\pi$-finite if it has finitely many components, all its homotopy groups are finite, and it is truncated in some finite degree. We write $\Spi$ for these spaces and $\Fn=\mathcal S_{\pi,\leq n}$. The empty space is allowed. A category is \emph{locally $n$-truncated} when its mapping spaces are $n$-types. In particular, $\Fn$ is locally $n$-truncated, and its core is an $(n+1)$-type. The category $\Spi$ is closed under finite limits and finite coproducts. Fibres over a $\pi$-finite base are $\pi$-finite exactly when their total space is $\pi$-finite. Mapping spaces between $\pi$-finite spaces are $\pi$-finite as well \cite[Proposition~3.4.4]{AnelPiFinite}. A uniform truncation bound is imposed on the objects of $\Fn$, but no uniform bound is imposed on the orders of their homotopy groups. For a bounded coherent $\infty$-topos $\X$, write \[ \C=\X^{\coh}_{\leq n}. \] We use the standard coherence convention in which the truncated coherent objects form a bounded $\infty$-pretopos \cite[Section~3.8]{BGHExodromy}. The full subcategory $\C$ is closed under finite limits and finite coproducts. Effective epimorphisms are computed in $\X$. The constant-object functor $\Delta:\Sps\to\X$ preserves finite limits and all colimits; its restriction to $\Fn$ takes values in $\C$. Indeed, the geometric morphism $\X\to\Sps$ is coherent: its target is a Stone $\infty$-topos~\cite[Corollary~4.4.15]{BGHExodromy}. Fixed truncation requires care with quotients. For instance, the groupoid with one object and nontrivial finite automorphism group $H$ has terms in $\mathcal F_0$, but its quotient $BH$ is a one-type. Thus the fixed subcategory $\mathcal F_0$ is not closed under all effective groupoid quotients in spaces. The following restricted quotient operation is the one needed in the paper. \begin{definition} A groupoid object $R_\bullet$ in a category with finite limits is \emph{$n$-efficient} if its arrow-to-endpoint map \[ R_1\longrightarrow R_0\times R_0 \] is $(n-1)$-truncated. For $n=0$, this says that the relation is a monomorphism. Truncatedness of maps can be expressed by the iterated diagonal criterion, so it is preserved by finite-limit functors and reflected by conservative finite-limit functors. \end{definition} \begin{lemma}[Quotients in the fixed range]\label{lem:efficient-quotient} An $n$-efficient groupoid object in $\C$ has an effective quotient in $\C$, computed in $\X$. An $n$-efficient groupoid object in $\Fn$ has a $\pi$-finite $n$-truncated quotient, computed in spaces. \end{lemma} \begin{proof} Let $Q=|R_\bullet|$ in $\X$. The groupoid is effective, so $R_0\to Q$ is an effective epimorphism and $R_1\simeq R_0\times_QR_0$. The diagonal of $Q$, after pullback along the effective epimorphism $R_0\times R_0\to Q\times Q$, is the endpoint map. Truncatedness is local for effective epimorphisms~\cite[Proposition~6.2.3.17]{LurieHTT}; hence $Q$ is $n$-truncated. Its coherence follows from closure under effective groupoid quotients of the bounded coherent category. These are the descent and exactness properties of coherent $\infty$-topoi; see~\cite[Sections~6.1--6.2]{LurieHTT} and~\cite[Section~3.8]{BGHExodromy}. For the assertion in spaces, the same argument bounds the truncation degree. The set $\pi_0Q$ is a quotient of $\pi_0R_0$, so it is finite. Every component contains the image of some point of $R_0$. The fibre of $R_0\to Q$ at this image is a fibre of $R_1\to R_0$, hence is $\pi$-finite. Its long exact homotopy sequence shows that the homotopy groups of $Q$ are finite. In degree one, the kernel is a quotient of $\pi_1R_0$ and the remaining cosets are indexed by a subset of the finite component set of the fibre. This also proves finiteness in that degree. \end{proof} \begin{remark}[The effective epimorphisms are intrinsic] For a map $A\to B$ in $\C$, its \v{C}ech nerve is $n$-efficient: its endpoint map is a pullback of the diagonal of $B$. By Lemma~\ref{lem:efficient-quotient}, its ambient quotient belongs to $\C$ and is also its quotient in that full subcategory. Thus a map in $\C$ is an ambient effective epimorphism exactly when it is the effective quotient map of its \v{C}ech nerve inside $\C$. In particular, equivalences of these categories preserve the class of effective epimorphisms. \end{remark} \begin{lemma}[Coherent descent along a finite atlas] \label{lem:coherent-descent} Let $P=\coprod_{i\in I}P_i\to1$ be an effective epimorphism with $I$ finite and $P_i\in\C$. Then \[ \C\simeq\lim_{[q]\in\Delta}\C/P^{q+1}. \] For $P_i\in\C$, the category $\C/P_i$ identifies with the coherent $n$-truncated objects of the slice $\X/P_i$. \end{lemma} \begin{proof} Effective descent gives the equivalence for the full topos and its slices. Truncatedness is local for effective epimorphisms. Since $P_i$ is itself $n$-truncated, a map to $P_i$ has an $n$-truncated total object exactly when it is $n$-truncated as an object of the slice; see also \cite[Lemma~5.5.6.14]{LurieHTT}. Coherence over a coherent base is the same in the slice and in $\X$~\cite[Paragraph~3.3.7]{BGHExodromy}. It remains to check that an object $Y$ reconstructed by descent is coherent when $Y\times P$ is coherent. The cover $Y\times P\to Y$ has coherent source, and its self-overlap is $(Y\times P)\times P$, which is coherent. The local criterion for $m$-coherence, first in degree zero and then in every positive degree, shows that $Y$ is coherent~\cite[Lemmas~3.6.2--3.6.3]{BGHExodromy}. Thus the full descent equivalence restricts to the displayed coherent subcategories. \end{proof} \section{Finite parameters on a coherent slice} \label{hr:sec-local} The local recognition argument first recovers maps between constants from components of their sections. Finite covers by sections then recover every coherent $n$-truncated object by induction on its truncation degree. Throughout this section, $n\geq0$ and $\mathcal F_n=\mathcal S_{\pi,\leq n}$. Let $\mathcal Y$ be a nondegenerate $\infty$-topos, with constant-object functor and global sections \[ c:\mathcal S\rightleftarrows\mathcal Y:\Gamma. \] The functor $c$ preserves finite limits and all colimits. In particular, it preserves the initial object. Nondegeneracy implies $\Gamma(0)=\varnothing$, since the initial object of an $\infty$-topos is strict. \begin{lemma}[Components of finite parameters] \label{hr:lem-components} Suppose that, for every $K\in\mathcal F_n$, the unit induces a surjection \begin{equation}\label{hr:eq-local-components} \pi_0K\longrightarrow\pi_0\Gamma(cK). \end{equation} Then the unit $K\to\Gamma(cK)$ is an equivalence for every $K\in\mathcal F_n$. Consequently \[ c:\mathcal F_n\longrightarrow\mathcal Y \] is fully faithful. \end{lemma} \begin{proof} First the map on components is injective. If $a,b\in K$ belong to different components, their path space is empty. Since $c$ preserves finite limits and the initial object, the path object between the constant sections $a,b:1\to cK$ is $c(\varnothing)=0$. Applying $\Gamma$ gives an empty path space. Thus their images cannot belong to the same component of $\Gamma(cK)$. For a point $a\in K$ and every $k\geq1$, preservation of finite limits by both $c$ and $\Gamma$ gives \[ \Omega^k_{c(a)}\Gamma(cK) \simeq\Gamma\bigl(c(\Omega_a^kK)\bigr). \] The space $\Omega_a^kK$ lies in $\mathcal F_n$. Applying \eqref{hr:eq-local-components} and the injectivity just proved to this loop space shows that the unit induces an isomorphism on $\pi_k$. The target $\Gamma(cK)$ is $n$-truncated, because $cK$ is $n$-truncated and global sections preserve limits. The unit is therefore an equivalence. Finally, for $U,V\in\mathcal F_n$, adjunction gives \[ \operatorname{Map}_{\mathcal Y}(cU,cV) \simeq\operatorname{Map}_{\mathcal S}(U,\Gamma(cV)) \simeq\operatorname{Map}_{\mathcal S}(U,V). \] \end{proof} The hypothesis concerns components of sections, but its test objects include finite homotopy types through degree $n$. It is therefore stronger than a condition imposed only on finite sets. Closure under loop spaces is what converts these component conditions into the comparison of all homotopy groups in the prescribed range. We next recognize the whole category from local sections. Suppose that $\mathcal Y$ is coherent. Its constant-object functor preserves coherent objects, since the target of the geometric morphism $\mathcal Y\to\mathcal S$ is Stone; see~\cite[Corollary~4.4.15]{BGHExodromy}. In particular, $cK$ is coherent for $K\in\mathcal F_n$. Write $\mathcal Y^{\mathrm{coh}}_{\leq n}$ for its coherent $n$-truncated objects. \begin{proposition}[Local recognition by finite sections] \label{hr:prop-local} The following conditions are equivalent. \begin{enumerate} \item The constant-object functor induces an equivalence \[ \mathcal F_n\xrightarrow{\sim} \mathcal Y^{\mathrm{coh}}_{\leq n}. \] \item Every $Y\in\mathcal Y^{\mathrm{coh}}_{\leq n}$ admits an effective epimorphism $\coprod_{a\in A}1\to Y$, where $A$ is a finite set. \item Every $Y\in\mathcal Y^{\mathrm{coh}}_{\leq n}$ admits an effective epimorphism $cK\to Y$ for some $K\in\mathcal F_n$. \end{enumerate} Under these conditions \eqref{hr:eq-local-components} holds. \end{proposition} \begin{proof} If (i) holds, choose one point in each of the finitely many components of the space representing $Y$. This gives (ii). Condition (ii) implies (iii) by using a finite discrete $K$. Conversely, a finite set of points meeting every component of $K$ gives an effective epimorphism from a finite discrete space to $K$. Applying $c$ and composing effective epimorphisms proves (ii) from (iii). Assume (ii). Every noninitial coherent $n$-truncated object has a global section: its covering finite sum of copies of $1$ must have at least one summand. To prove \eqref{hr:eq-local-components}, let $t:1\to cK$ be a section. Choose representatives $k_a\in K$ for the finite set $\pi_0K$. Pulling the effective epimorphism $\coprod_a1\to cK$ back along $t$ gives a finite cover of $1$ by the coherent objects \[ E_a=1\times_{cK}1, \] where the two maps to $cK$ are $t$ and the constant section $k_a$. Each $E_a$ is $(n-1)$-truncated. Since $\mathcal Y$ is nondegenerate, at least one of the $E_a$ is noninitial. It has a section by (ii), and that section is a homotopy from $t$ to $k_a$. Lemma~\ref{hr:lem-components} now proves full faithfulness of $c|_{\mathcal F_n}$. We prove essential surjectivity by induction on the truncation degree $k$, starting with $k=-1$. A coherent subterminal object is either initial or has a section by (ii). In the second case its monomorphism to $1$ is an equivalence. Thus every coherent $(-1)$-truncated object is constant. Let $0\leq k\leq n$ and let $Y$ be coherent and $k$-truncated. Choose an effective epimorphism $cA=\coprod_{a\in A}1\to Y$ with $A$ finite. For each ordered pair $(a,b)$, its path object \[ R_{ab}=1\times_Y1 \] is coherent and $(k-1)$-truncated. By induction it is constant on a $\pi$-finite $(k-1)$-type. The kernel pair of $cA\to Y$ is the finite sum $\coprod_{a,b}R_{ab}$, so it too is in the image of $c|_{\mathcal F_n}$. For $k=0$ its summands are initial or terminal, and its total space is a finite discrete space. The essential image of this fully faithful functor is closed under finite limits. Consequently the entire \v{C}ech nerve, including all its higher compatibilities, lifts to a groupoid object $R_\bullet$ in $\mathcal F_n$. Realize it in spaces, writing $S=|R_\bullet|$. Its object space is the finite discrete space $A$, and the fibre of $R_1\to A\times A$ over $(a,b)$ is the $\pi$-finite $(k-1)$-type representing $R_{ab}$. Effectivity in spaces gives $R_1\simeq A\times_SA$. Thus the path spaces of $S$ are $(k-1)$-truncated and $\pi$-finite; its components are a quotient of the finite set $A$. It follows that $S$ is a $\pi$-finite $k$-type. Finally, preservation of realizations by $c$ gives \[ cS\simeq|cR_\bullet|\simeq Y. \] This completes the induction and the proof of (i). \end{proof} Finite constant covers supply parameter elimination and recover kernel presentations by induction. The decrease of truncation degree is explicit: path objects of a $k$-truncated object have degree $k-1$. \begin{example}[Parameter elimination alone does not present objects] Let $\mathcal Y=\Fun([1],\mathcal S)$. The global sections of a constant diagram are its constant value, so $\Gamma(cK)\simeq K$ for every space $K$. Nevertheless the coherent zero-truncated object $(\varnothing\to *)$ is noninitial and has no section. A map from a constant diagram $(K\to K)$ to it forces $K=\varnothing$, and cannot be an effective epimorphism. Thus even the full comparison on constant mapping spaces does not imply the finite-section hypothesis. \end{example} \section{Recognition from a finite atlas} \label{hr:sec-atlas} We apply the local recognition result to the slices over a finite cover. The resulting slice equivalences identify the overlaps and their transport maps; effective descent then recovers the category. Let $\mathcal X$ be a bounded coherent $\infty$-topos and put \[ \mathcal C=\mathcal X^{\mathrm{coh}}_{\leq n}. \] Let $\Delta:\mathcal S\to\mathcal X$ be its constant-object functor. As recalled in Section~\ref{sec:foundations}, it sends $\mathcal F_n$ into $\mathcal C$. Lemma~\ref{lem:coherent-descent} supplies effective descent in $\mathcal C$ and the identification $\mathcal C/P=(\mathcal X/P)^{\mathrm{coh}}_{\leq n}$ for $P\in\mathcal C$. \begin{theorem}[Recognition from finite local parameters] \label{hr:thm-atlas} Suppose there are finitely many noninitial objects $P_i\in\mathcal C$, indexed by a finite set $I$, such that \[ P=\coprod_{i\in I}P_i\longrightarrow1 \] is an effective epimorphism. Suppose that, for each $i$, every $Y\in\mathcal C/P_i$ admits an effective epimorphism \[ \coprod_{a\in A}P_i\longrightarrow Y \quad\text{over }P_i, \] where $A$ is a finite set. Let $\mathcal G$ be the full subcategory of $\mathcal C$ on the objects $P_i$, and put $\mathcal M=\mathcal G^{\mathrm{op}}$. Then all morphisms of $\mathcal G$ are equivalences, and $\mathcal M$ is a $\pi$-finite $(n+1)$-type. The functor \begin{equation}\label{hr:eq-recognition} \mathcal C\longrightarrow \operatorname{Fun}(\mathcal M,\mathcal F_n), \qquad A\longmapsto \bigl(i\longmapsto\operatorname{Map}_{\mathcal C}(P_i,A)\bigr) \end{equation} is an equivalence. Under it, $\Delta K$ corresponds to the constant functor with value $K$. \end{theorem} \begin{proof} If $I$ is empty, the cover forces $\mathcal X$ to be degenerate; then $\mathcal C$ is terminal and $\mathcal M=\varnothing$, so the assertion holds. Otherwise apply Proposition~\ref{hr:prop-local} to $\mathcal X/P_i$. Its nondegeneracy follows from $P_i\ne0$. We obtain equivalences \begin{equation}\label{hr:eq-slice-equivalence} \Phi_i:\mathcal F_n\xrightarrow{\sim}\mathcal C/P_i, \qquad K\longmapsto P_i\times\Delta K. \end{equation} The inverse is the restriction of global sections in the slice. In particular, for $A\in\mathcal C$, \begin{equation}\label{hr:eq-evaluation} \omega_i(A):=\operatorname{Map}_{\mathcal C}(P_i,A) \simeq\Phi_i^{-1}(P_i\times A) \quad\text{lies in }\mathcal F_n. \end{equation} Consider a morphism $f:P_i\to P_j$. Under $\Phi_j$, its object in $\mathcal C/P_j$ corresponds to some $F\in\mathcal F_n$. Taking slices of \eqref{hr:eq-slice-equivalence} gives \[ \mathcal C/P_i\simeq(\mathcal C/P_j)/f \simeq\mathcal F_n/F. \] The identity $f^*\Phi_j=\Phi_i$ identifies the functor $F^*:\mathcal F_n\to\mathcal F_n/F$, $K\mapsto F\times K$, with an equivalence. Its full faithfulness, applied to $1$ and $F$, says that the map \[ F=\operatorname{Map}(1,F)\longrightarrow \operatorname{Map}(F,F) \] sending a point to the corresponding constant map is an equivalence. In particular, the identity of $F$ is homotopic to a constant map. Thus $F$ is contractible, and $f$ is an equivalence. This proves that $\mathcal G$ is an $\infty$-groupoid. Its mapping spaces are $\pi$-finite $n$-types by \eqref{hr:eq-evaluation}. It has finitely many objects, so its space of components is finite and its loop spaces are $\pi$-finite $n$-types. Hence $\mathcal M$ is a $\pi$-finite $(n+1)$-type. It remains to prove \eqref{hr:eq-recognition}. By Lemma~\ref{lem:coherent-descent}, descent along $P\to1$ gives \begin{equation}\label{hr:eq-cech-categories} \mathcal C\simeq \lim_{[q]\in\Delta}\mathcal C/P^{q+1}. \end{equation} Finite coproducts are disjoint and universal. For a tuple $\mathbf i=(i_0,\ldots,i_q)$, put $P_{\mathbf i}=P_{i_0}\times\cdots\times P_{i_q}$. In the slice over $P_{i_0}$ this object corresponds to \[ F_{\mathbf i} =\prod_{k=1}^q \operatorname{Map}_{\mathcal C}(P_{i_0},P_{i_k}). \] Consequently \begin{equation}\label{hr:eq-overlap-categories} \mathcal C/P^{q+1} \simeq\prod_{\mathbf i}\mathcal F_n/F_{\mathbf i} \simeq\prod_{\mathbf i} \operatorname{Fun}(F_{\mathbf i},\mathcal F_n). \end{equation} The last equivalence is straightening for spaces. It restricts to $\pi$-finite $n$-types because both base and fibres are $\pi$-finite $n$-types. The slice counits defining these equivalences are natural, and straightening is natural under base change. Thus the equivalences respect the face and degeneracy maps with their coherences. Explicitly, a point $u:P_i\to P_j$ of an overlap carries $\omega_j(A)$ to $\omega_i(A)$ by precomposition; the maps on multiple overlaps are composition and insertion of identities. Changing the distinguished index of a multiple overlap uses the inverse of $u$, which exists by the preceding argument. Thus the cosimplicial diagram in \eqref{hr:eq-overlap-categories} is the descent diagram for a functor on $\mathcal G^{\mathrm{op}}$. Equivalently, it is obtained from the \v{C}ech nerve of the map of spaces $I\to\mathcal M$ by applying $\operatorname{Fun}(-,\mathcal F_n)$. The realization of that nerve is $\mathcal M$, and functor categories turn colimits in the source into limits. Equations \eqref{hr:eq-cech-categories}--\eqref{hr:eq-overlap-categories} therefore prove \eqref{hr:eq-recognition}. The unit equivalences in Lemma~\ref{hr:lem-components} identify each $\omega_i(\Delta K)$ with $K$, compatibly with transport, which proves the assertion about constants. \end{proof} \begin{corollary}[Independence of the atlas] \label{hr:cor-atlas-independence} If two finite families satisfy the hypotheses of Theorem~\ref{hr:thm-atlas}, their associated groupoids are equivalent. Both embed as full, essentially surjective subgroupoids of the groupoid associated with their union. \end{corollary} \begin{proof} Write the two families as $(P_i)$ and $(Q_j)$. Their union again satisfies the local hypotheses, so every morphism between its objects is an equivalence. Pull the cover $\coprod_iP_i\to1$ back to $Q_j$. Under $\Phi_{Q_j}^{-1}$ the resulting effective epimorphism becomes \[ \coprod_i\operatorname{Map}_{\mathcal C}(Q_j,P_i) \longrightarrow1. \] Its source is nonempty. Thus $Q_j$ admits a morphism to some $P_i$, and this morphism is an equivalence. The same argument with the families interchanged proves the assertion. \end{proof} \subsection{The groupoid of models} \label{hr:subsec-models} \begin{lemma}[Preservation of constants] \label{hr:lem-constants-automatic} Let $H:\mathcal F_n\to\mathcal F_n$ preserve finite limits, finite coproducts, and effective epimorphisms. Then the Yoneda transformation $\mathrm{id}_{\mathcal F_n}\to H$ is an equivalence, and its space of choices is contractible. \end{lemma} \begin{proof} The identity functor of $\mathcal F_n$, regarded as a space-valued functor, is represented by the point. Yoneda gives \[ \operatorname{Nat}(\mathrm{id}_{\mathcal F_n},H) \simeq H(*)\simeq *. \] Write $\eta$ for its transformation. For $K\in\mathcal F_n$, choose a finite set of points meeting every component of $K$. The resulting effective epimorphism $A\to K$ remains an effective epimorphism under $H$. Since $H$ preserves finite coproducts and the terminal object, $\eta_A:A\to H(A)$ is an equivalence. Naturality now shows that $\pi_0\eta_K$ is surjective. If $a,b\in K$ belong to different components, their path space is empty. Preservation of finite limits and the initial object shows that the path space between $\eta_K(a)$ and $\eta_K(b)$ is also empty. This proves injectivity on components. For every basepoint $a$, finite-limit preservation identifies $\Omega^k\eta_K$ with $\eta_{\Omega_a^kK}$. The same component argument therefore gives isomorphisms on all homotopy groups. Both sides are $n$-types, so $\eta_K$ is an equivalence. The contractible space of Yoneda transformations thus consists entirely of equivalences. \end{proof} Let $\operatorname{Mod}_n(\mathcal C)$ be the full $\infty$-subcategory of $\operatorname{Fun}(\mathcal C,\mathcal F_n)$ on the functors preserving finite limits, finite coproducts, and effective epimorphisms. Its morphisms are all natural transformations. For each such functor $F$, Lemma~\ref{hr:lem-constants-automatic} applied to $F\Delta$ supplies a canonical equivalence $F\Delta\simeq\mathrm{id}_{\mathcal F_n}$. \begin{theorem}[Recognition of all models] \label{hr:thm-models} Under the hypotheses of Theorem~\ref{hr:thm-atlas}, each $\omega_i=\operatorname{Map}_{\mathcal C}(P_i,-)$ is a model, and evaluation induces an equivalence \[ \mathcal M\xrightarrow{\sim} \operatorname{Mod}_n(\mathcal C). \] For every $i,j$, its map on mapping spaces is the Yoneda equivalence \[ \operatorname{Map}_{\mathcal M}(i,j) =\operatorname{Map}_{\mathcal C}(P_j,P_i) \simeq\operatorname{Nat}(\omega_i,\omega_j). \] In particular, every natural transformation between models is an equivalence, and $\operatorname{Mod}_n(\mathcal C)$ is a $\pi$-finite $(n+1)$-groupoid. \end{theorem} \begin{proof} The description of $\omega_i$ in \eqref{hr:eq-evaluation} expresses it as pullback to $P_i$, followed by the equivalence $\Phi_i^{-1}$. It therefore preserves finite limits, finite coproducts, and effective epimorphisms. If the atlas is empty, $\mathcal C$ is degenerate. A model would have to send its initial and terminal object both to $\varnothing$ and to $*$, so there are no models, as required. Otherwise, let $F$ be a model. Since $F$ preserves the finite sum and the cover of the terminal object, \[ F(P)=\coprod_iF(P_i)\longrightarrow1 \] is an effective epimorphism of spaces. Choose $i$ and a point $a\in F(P_i)$. Yoneda associates to $a$ a natural transformation $\omega_i\to F$. For every $A\in\mathcal C$, the counit of the slice equivalence gives a natural equivalence over $P_i$, \[ P_i\times\Delta\omega_i(A)\xrightarrow{\sim}P_i\times A. \] Applying $F$, using preservation of products and the canonical identification of constants from Lemma~\ref{hr:lem-constants-automatic}, and taking the fibre at $a$ gives an equivalence \[ \omega_i(A)\xrightarrow{\sim}F(A). \] It is exactly the component of the Yoneda transformation and is natural in $A$. This proves essential surjectivity. Yoneda gives $\operatorname{Nat}(\omega_i,\omega_j) \simeq\operatorname{Map}_{\mathcal C}(P_j,P_i)$. Every arrow on the right is an equivalence by Theorem~\ref{hr:thm-atlas}, so every transformation on the left is an equivalence. Thus evaluation is fully faithful, and all natural transformations between arbitrary models are equivalences by the essential-surjectivity assertion. \end{proof} \subsection{The converse construction} \begin{proposition}[The converse construction] \label{hc:prop-converse} Let $M$ be a $\pi$-finite $(n+1)$-type and put \[ \mathcal X_M=\operatorname{Fun}(M,\mathcal S), \qquad \mathcal C_M=\operatorname{Fun}(M,\mathcal F_n). \] Then $\mathcal X_M$ is a bounded coherent $\infty$-topos and $\mathcal C_M=(\mathcal X_M)^{\mathrm{coh}}_{\leq n}$. Choose one point $x_i$ in each component of $M$ and let \[ P_i=\operatorname{Map}_M(x_i,-)\in\mathcal C_M. \] This finite family satisfies the hypotheses of Theorem~\ref{hr:thm-atlas}. Its groupoid $\mathcal M$ is equivalent to $M$, compatibly with evaluation and the constant-object functors. \end{proposition} \begin{proof} Straightening identifies $\operatorname{Fun}(M,\mathcal S)$ with $\mathcal S/M$. A $\pi$-finite space is a truncated coherent object of $\mathcal S$, so the slice is bounded coherent; see~\cite[Examples~3.2.8 and~3.3.5, Paragraph~3.3.7]{BGHExodromy}. In this slice, coherence of $Y\to M$ is equivalent to coherence of its total space, since the base is coherent. For an $n$-truncated map to the $\pi$-finite base $M$, its total space is $\pi$-finite if and only if its fibres are $\pi$-finite. One direction uses finite limits of $\pi$-finite spaces. For the other, use the long exact sequence of homotopy groups on each of the finitely many base components; the total space is truncated, and its homotopy groups and set of components are finite. This proves the description of $\mathcal C_M$. The object $P_i$ corresponds to the point $x_i:*\to M$. Its total space is coherent, and its fibres are path spaces in $M$, which are $\pi$-finite $n$-types. Thus $P_i$ is coherent and $n$-truncated in $\mathcal X_M$. The map $\coprod_iP_i\to1$ is an effective epimorphism because the chosen points meet every component of $M$. Taking a slice at $x_i:*\to M$ identifies \[ \mathcal X_M/P_i\simeq\mathcal S, \qquad \mathcal C_M/P_i\simeq\mathcal F_n. \] Under this equivalence $P_i\times\Delta K$ corresponds to $K$. Every $K\in\mathcal F_n$ has an effective epimorphism from a finite discrete space, obtained by choosing one point per component. The finite-section hypothesis therefore holds. Finally, Yoneda gives \[ \operatorname{Map}_{\mathcal C_M}(P_i,P_j) \simeq\operatorname{Map}_M(x_j,x_i). \] The chosen points meet all components, so the opposite of the full subgroupoid on the $P_i$ is equivalent to $M$. The Yoneda equivalence identifies $\operatorname{Map}_{\mathcal C_M}(P_i,A)$ with $A(x_i)$, which proves the compatibility assertions. \end{proof} The standard facts about truncated coherent spaces and their slices in this proof can also be expressed intrinsically through the exact structure of $\pi$-finite spaces; see~\cite{AnelPiFinite}. Theorem~\ref{hr:thm-atlas} and Proposition~\ref{hc:prop-converse} give a recognition of finite homotopy semantics by the finite local-section condition. \section{Finite descent and sharpness} \label{hr:sec-coherence} Truncation bounds the simplicial degrees needed for descent. Mapping spaces are $n$-types, whereas the core of a locally $n$-truncated category is an $(n+1)$-type; objects therefore require one additional degree. The totalization results used here are classical; compare \cite[Lemmas~3.4.2--3.4.3]{AnelPiFinite} and \cite[Proposition~A.1(2)]{HesselholtPstragowskiDirac}. We give the space-valued argument to fix the indexing. The convention here uses $n$-truncated mapping spaces, whereas an $r$-category in the cited formulation has $(r-1)$-truncated mapping spaces. Let $\Delta_{\leq m}$ be the full subcategory of $\Delta$ on $[0],\ldots,[m]$. Limits below are homotopy limits. \begin{lemma}[Finite totalization] \label{hr:lem-finite-tot} For a cosimplicial diagram of $n$-truncated spaces $Z^\bullet$, restriction induces an equivalence \[ \lim_{\Delta} Z^\bullet \xrightarrow{\sim} \lim_{\Delta_{\leq n+1}} Z^\bullet. \] \end{lemma} \begin{proof} Put $m=n+1$ and let $j:\Delta_{\leq m}\to\Delta$ be the inclusion. The left Kan extension of the constant point has value \[ (\operatorname{Lan}_j *)([q]) \simeq B(\Delta_{\leq m}/[q]). \] Sending a map $[p]\to[q]$ to its image retracts this indexing category, up to homotopy, onto the poset of nonempty subsets of $\{0,\ldots,q\}$ of cardinality at most $m+1$. Its classifying space is the barycentric subdivision of the $m$-skeleton of $\Delta^q$. This skeleton is $(m-1)$-connected: the full simplex is obtained by adding cells of dimensions at least $m+1$. Hence the natural map $\operatorname{Lan}_j*\to *$ becomes an equivalence after objectwise $n$-truncation. Since $Z^\bullet$ is objectwise $n$-truncated, mapping into it depends only on that objectwise truncation. Adjunction therefore gives \begin{align*} \lim_{\Delta}Z^\bullet &\simeq\operatorname{Map}_{\operatorname{Fun}(\Delta,\mathcal S)} (*,Z^\bullet)\\ &\simeq\operatorname{Map}_{\operatorname{Fun}(\Delta,\mathcal S)} (\operatorname{Lan}_j*,Z^\bullet)\\ &\simeq\lim_{\Delta_{\leq m}}Z^\bullet. \end{align*} \end{proof} \begin{theorem}[Finite descent for objects and maps] \label{hr:thm-finite-descent} Let $\mathcal D^\bullet$ be a cosimplicial diagram of locally $n$-truncated $\infty$-categories. Then \begin{equation}\label{hr:eq-object-cutoff} \lim_{\Delta}\mathcal D^\bullet \xrightarrow{\sim} \lim_{\Delta_{\leq n+2}}\mathcal D^\bullet. \end{equation} For objects $A,B$ of the limit, their mapping space is \begin{equation}\label{hr:eq-map-cutoff} \operatorname{Map}(A,B) \simeq\lim_{[q]\in\Delta_{\leq n+1}} \operatorname{Map}_{\mathcal D^q}(A_q,B_q). \end{equation} In particular, the reconstruction in Theorem~\ref{hr:thm-atlas} uses \v{C}ech degrees at most $n+2$ for objects and at most $n+1$ for maps. \end{theorem} \begin{proof} Mapping spaces in a limit of $\infty$-categories are the limits of the mapping spaces of its compatible objects. These mapping spaces are $n$-truncated, so Lemma~\ref{hr:lem-finite-tot} proves \eqref{hr:eq-map-cutoff}. For the assertion about categories, use the complete Segal nerve \[ N(\mathcal D)_r= \operatorname{Fun}([r],\mathcal D)^{\simeq}. \] It preserves limits and detects equivalences. If $\mathcal D$ is locally $n$-truncated, so is its functor category on $[r]$, and the core of that functor category is an $(n+1)$-type. For each $r$, Lemma~\ref{hr:lem-finite-tot}, with $n+1$ in place of $n$, therefore identifies the full cosimplicial limit of these nerve spaces with the limit through degree $n+2$. This proves \eqref{hr:eq-object-cutoff} levelwise on the complete Segal nerve. \end{proof} \subsection{Finite simplicial presentations} \begin{theorem}[A finite simplicial presentation] \label{hc:thm-simplicial} Let $M$ be a $\pi$-finite $(n+1)$-type. Choose a Kan simplicial set $G_\bullet$ with finite sets of simplices in every degree and an equivalence $|G_\bullet|\simeq M$. Such a model can be chosen to be $(n+2)$-coskeletal. Then \begin{equation}\label{hc:eq-category} \operatorname{Fun}(M,\mathcal F_n) \simeq \lim_{[q]\in\Delta_{\leq n+2}}\mathcal F_n^{G_q}. \end{equation} For $A,B\in\operatorname{Fun}(M,\mathcal F_n)$, write $A_q,B_q:G_q\to\mathcal F_n$ for their restrictions along the colimit cocone. There is a natural equivalence \begin{equation}\label{hc:eq-maps} \operatorname{Map}(A,B) \simeq \lim_{[q]\in\Delta_{\leq n+1}} \prod_{g\in G_q} \operatorname{Map}_{\mathcal F_n}(A_q(g),B_q(g)). \end{equation} \end{theorem} \begin{proof} The existence of a degreewise finite Kan presentation and its coskeletal truncation is the finite Kan model construction for $\pi$-finite types; see~\cite[Proposition~3.2.3]{AnelPiFinite}. Since $M$ is the colimit of $G_\bullet$ in spaces, \[ \operatorname{Fun}(M,\mathcal F_n) \simeq\lim_{\Delta}\operatorname{Fun}(G_q,\mathcal F_n) =\lim_{\Delta}\mathcal F_n^{G_q}. \] Each of the finite-product categories $\mathcal F_n^{G_q}$ is locally $n$-truncated. Applying Theorem~\ref{hr:thm-finite-descent} gives \eqref{hc:eq-category}; its mapping-space formula gives \eqref{hc:eq-maps}. \end{proof} Here finiteness has two precise meanings: only the indicated simplicial degrees enter the limit, and each indexing set $G_q$ in those degrees is finite. The categories $\mathcal F_n$ still contain all $\pi$-finite $n$-types. The recognition statement does not impose a bound on their cardinalities or on the orders of their homotopy groups. \begin{center} \begin{tabular}{llll} \toprule Family level & Model-space bound & Maps through & Objects through\\ \midrule $n=0$ & $1$-type & degree $1$ & degree $2$\\ $n=1$ & $2$-type & degree $2$ & degree $3$\\ $n=2$ & $3$-type & degree $3$ & degree $4$\\ $n$ & $(n+1)$-type & degree $n+1$ & degree $n+2$\\ \bottomrule \end{tabular} \end{center} \subsection{Sharpness for truncated cosimplicial descent} \begin{proposition}[Sharpness of the coherence degrees] \label{hr:prop-cutoff-sharp} For every $n\geq0$, the degree $n+1$ in Lemma~\ref{hr:lem-finite-tot} cannot be replaced by $n$, even for cosimplicial $\pi$-finite $n$-types. The degree $n+2$ in \eqref{hr:eq-object-cutoff} cannot be replaced by $n+1$, even for cosimplicial $\pi$-finite $\infty$-groupoids. \end{proposition} \begin{proof} Let $G=C_2=\{1,g\}$ and let $A=\mathbb F_3$ with the action \[ ga=\varepsilon a,\qquad \varepsilon=(-1)^{n+1}. \] Use the usual group-cochain cosimplicial space \[ Z^q=K(A,n)^{G^q}. \] Its totalization is the homotopy fixed-point space $K(A,n)^{hG}$. The normalized cochain group in every degree is $A$: a normalized cochain is determined by its value on $(g,\ldots,g)$. All internal terms in its coboundary vanish, because $g^2=1$ inserts an identity. Thus the differential on normalized cochains is multiplication by \[ d^q=\varepsilon+(-1)^{q+1}. \] In particular, $d^{n-1}=0$ for $n>0$, whereas $d^n=2\varepsilon$ is invertible in $\mathbb F_3$. The degree-$n$ components of partial totalization are consequently \[ \pi_0\operatorname{Tot}_n Z^\bullet\cong\mathbb F_3, \qquad \pi_0\operatorname{Tot} Z^\bullet \cong H^n(G,A)=0. \] For $n=0$, the first equality just says that $\operatorname{Tot}_0=A$, whereas full totalization is the fixed-point set of the sign action, which contains only zero. For $n>0$, normalization in the simplicial direction places $A$ in homological degree $n$. Normalization in the cosimplicial direction then gives the group-cochain complex as a single row. The component group of partial totalization through degree $n$ is therefore $C^n/\operatorname{im}d^{n-1}$; the component group of full totalization is $\ker d^n/\operatorname{im}d^{n-1}$. Thus through degree $n$ there is no cocycle condition on the top cochain, and degree $n+1$ imposes $d^n=0$. For the categorical assertion, perform the same construction with $n+1$ in place of $n$ and regard each resulting $(n+1)$-type as an $\infty$-groupoid. Its mapping spaces are $n$-truncated. Its limit through degree $n+1$ has three components, while the full limit has one component. Thus that finite limit is not equivalent to the full limit category. \end{proof} \subsection{Sharpness for finite homotopy actions} \label{hs:sec-finite-actions} The two cutoffs are optimal for the descent diagrams occurring in finite homotopy semantics. Put $G=C_2=\{1,g\}$ and \[ \mathcal D^q=\mathcal F_n^{G^q},\qquad \mathcal D_{\leq m}=\lim_{\Delta_{\leq m}}\mathcal D^\bullet. \] The structure maps are pullback along the nerve of $G$. Thus $\lim_\Delta\mathcal D^\bullet\simeq\operatorname{Fun}(BG,\mathcal F_n)$. Write $R_m$ for restriction from this full limit to $\mathcal D_{\leq m}$. \begin{proposition}[Sharpness within finite homotopy actions] \label{hs:prop-sharp-actions} For every $n\geq0$, the functor $R_n$ is not full on homotopy categories. The functor $R_{n+1}$ is not essentially surjective. Consequently neither the mapping cutoff $n+1$ nor the object cutoff $n+2$ can be decreased, even for the diagrams $\mathcal F_n^{C_2^q}$. \end{proposition} \begin{proof} We first describe precisely the partial descent spaces used below. Let $B_\bullet G$ be the nerve of $G$, and put $B_m=|\operatorname{sk}_m B_\bullet G|$. For every space $T$, \begin{equation}\label{hs:eq-skeleton} \lim_{\Delta_{\leq m}}T^{G^q} \simeq\operatorname{Map}(B_m,T). \end{equation} One way to obtain this equivalence is to represent $T$ by a Kan complex. The cosimplicial space $T^{G^q}$ is Reedy fibrant: its matching maps restrict functions to the degenerate simplices of $B_qG$, and hence are projections between products of Kan complexes. Its partial totalization is therefore the derived limit on the left. The end--coend adjunction identifies this partial totalization with maps from the realization of the simplicial $m$-skeleton, proving \eqref{hs:eq-skeleton}. Since passage to the core preserves limits, this also gives \begin{equation}\label{hs:eq-core} (\mathcal D_{\leq m})^{\simeq} \simeq\operatorname{Map}(B_m,\mathcal F_n^{\simeq}). \end{equation} The standard bar model of $BC_2$ has one nondegenerate simplex in every degree. Its skeletal filtration is the usual $B_m\simeq\mathbb{RP}^{m}\subset\mathbb{RP}^{\infty}\simeq BC_2$. Here is the cochain calculation we shall use twice. Let $A=\mathbb F_3$, and let $g$ act on $A$ by $\varepsilon\in\{1,-1\}$. A normalized degree-$q$ group cochain is determined by its value on $(g,\ldots,g)$, so its group is $A$ in every degree. All internal terms of the bar coboundary vanish: multiplying two adjacent $g$'s inserts the identity. In these coordinates the differential is \begin{equation}\label{hs:eq-differential} d^q a=\bigl(\varepsilon+(-1)^{q+1}\bigr)a. \end{equation} This is also the cellular cochain complex of the skeletal bar model, with the corresponding choice of orientations and local coefficients. Truncating at $B_m$ removes the outgoing differential in degree $m$. \emph{Step 1: Maps.} Take the terminal local system $U$, and let $V$ have fibre $K(A,n)$ with the strict linear $G$-action $\varepsilon=(-1)^{n+1}$. These are genuine objects of $\operatorname{Fun}(BG,\mathcal F_n)$. Their mapping cosimplicial space is the group-cochain diagram $K(A,n)^{G^q}$, with the first coface twisted by this action. Its partial totalization computes sections of the associated $K(A,n)$-bundle on $B_m$. For $n\geq1$, components of those sections at $m=n$ are \[ \pi_0\operatorname{Map}_{\mathcal D_{\leq n}}(R_nU,R_nV) \cong H^n(B_n;A_\varepsilon)\cong A. \] Indeed, \eqref{hs:eq-differential} gives $d^{n-1}=0$. For the full mapping space the next differential is present, and $d^n=2\varepsilon$ is invertible in $\mathbb F_3$. Hence \[ \pi_0\operatorname{Map}_{\operatorname{Fun}(BG,\mathcal F_n)}(U,V) \cong H^n(BG;A_\varepsilon)=0. \] The zero on the right denotes a single component. Restriction therefore misses both nonzero partial components. For $n=0$, the partial mapping set is $A$, while the full mapping set is the fixed set of the sign action, namely $\{0\}$. This proves the assertion about $R_n$ in all degrees. \emph{Step 2: Objects for $n\geq1$.} Suppose $n\geq1$ and put $r=n+1\geq2$. We use the component of $K=K(A,n)$ in $\mathcal F_n^{\simeq}$, namely $B\operatorname{Aut}(K)$. There is an equivalence of $\infty$-groups \begin{equation}\label{hs:eq-affine} \operatorname{Aut}(K(A,n)) \simeq K(A,n)\rtimes\operatorname{Aut}(A). \end{equation} For completeness, choose a simplicial abelian model of $K(A,n)$. Translations and linear automorphisms give the map in \eqref{hs:eq-affine}, compatibly with composition. Evaluation at zero identifies the fibre of the target over zero with pointed self-equivalences. The pointed mapping space has components $\operatorname{Hom}(A,A)$ and has no positive homotopy groups: its degree-$j$ homotopy group is $\widetilde H^{n-j}(K(A,n);A)=0$ for $1\leq j\leq n$, and it is $n$-truncated. Restricting to self-equivalences gives the discrete fibre $\operatorname{Aut}(A)$. Thus the affine map is an equivalence on the base and on every fibre, proving \eqref{hs:eq-affine}. Since $\operatorname{Aut}(A)=C_2$, delooping gives the split fibration \begin{equation}\label{hs:eq-band-fibration} K(A,r)\longrightarrow E:=B\operatorname{Aut}(K) \simeq K(A,r)\mathbin{\!//\!}C_2 \xrightarrow{p}BC_2. \end{equation} The zero of $K(A,r)$ supplies a section. We call the composite to $BC_2$ the \emph{band}; it records the induced action on $A=\pi_n(K)$. Choose $\rho:G\to C_2$ with $\rho(g)=\varepsilon=(-1)^{r+1}=(-1)^{n+2}$. Fix its restriction $b_m:B_m\to BC_2$. The space of lifts of $b_m$ to $E$ is the section space of the associated $K(A,r)$-bundle. Consequently its components are \begin{equation}\label{hs:eq-banded-classes} \pi_0\operatorname{Map}_{/BC_2}(b_m,E) \cong H^r(B_m;A_\varepsilon). \end{equation} This is the usual cochain description of an Eilenberg--Mac Lane bundle: choices on $r$-cells are $r$-cochains, changes of choices on $(r-1)$-cells add coboundaries, and extension over $(r+1)$-cells imposes the cocycle condition. There are no additional obstruction groups, because the fibre has only the homotopy group $A$ in degree $r$. By \eqref{hs:eq-differential}, \[ d^{r-1}=0,\qquad d^r=2\varepsilon\in\mathbb F_3^\times. \] It follows that the banded partial objects over $B_r$ have component set $A$, whereas every lift over $B_{r+1}$ restricts to the zero component. In particular, a nonzero class $a\in A$ does not extend with its band fixed. To prove nonextendibility up to equivalence, we must also account for changes of band identification. For every $m\geq2$, the inclusion $B_m\to BG$ induces an isomorphism on fundamental groups. Since the target $BC_2$ is a $1$-type, its mapping space is the groupoid of homomorphisms $G\to C_2$ and their conjugacies. Thus the component containing $b_m$ is \[ \operatorname{Map}(B_m,BC_2)_{b_m}\simeq BC_2. \] Its loop group is the centralizer $C_{C_2}(\rho(G))=C_2$. For the split fibration \eqref{hs:eq-band-fibration}, a gauge element $h\in C_2$ acts on the lift space through the coefficient automorphism $a\mapsto ha$. In particular it sends the zero section to the zero section. Explicitly, applying the same $h$ in every fibre of the associated bundle sends each cochain to $h$ times that cochain and commutes with \eqref{hs:eq-differential}. The elementary component sequence of this mapping-space fibration now says that the unbanded homotopy classes lying over the component of $b_m$ are precisely \begin{equation}\label{hs:eq-gauge-orbits} H^r(B_m;A_\varepsilon)/C_2. \end{equation} Indeed, two points of the fibre become connected in the total space exactly when their components are related by the monodromy of a loop in the base. Restriction from $B_{r+1}$ to $B_r$ respects these actions. Its banded image is zero, hence its unbanded image is the orbit $\{0\}$. The nonzero classes form the different orbit $\{1,-1\}$. Moreover a different homomorphism $\rho'$ cannot help: conjugacy in the abelian group $C_2$ does not change $\rho$, and all bands on $B_r$, for $r\geq2$, already come from unique components of bands on $BG$. Thus the nonzero partial object is not equivalent to the restriction of any object over $B_{r+1}$, or over $BG$. Equation~\eqref{hs:eq-core} proves the failure of essential surjectivity of $R_{n+1}$ when $n\geq1$. \emph{Step 3: Objects for $n=0$.} For $n=0$ one has $r=1$, and the preceding argument using $\pi_1(B_r)=G$ is unavailable: $B_1\simeq S^1$ has fundamental group $\mathbb Z$. We therefore handle this case directly. Let $K=A$ be the three-element set, so $\operatorname{Aut}(K)=S_3=A\rtimes C_2$. The map \[ B_1\simeq S^1\longrightarrow BS_3 \] which sends its generator to the translation $x\mapsto x+1$ is a degree-one partial descent object with trivial band in $C_2$, as required by $\varepsilon=(-1)^{r+1}=1$. It cannot extend to $B_2$: the relation imposed there is $g^2=1$, whereas this translation has order three. Equivalence after forgetting the band only conjugates its monodromy in $S_3$, and conjugation preserves order. More explicitly, conjugation by translations fixes the translation subgroup, and conjugation by its linear $C_2$ factor sends $1$ to $-1$. Its nonzero orbit still does not meet zero. Hence no change of band or gauge can turn this partial object into a genuine $C_2$-action. This proves the remaining case and completes the proof. \end{proof} \begin{remark} The mapping counterexample uses two genuine full descent objects and a nonextendible partial map between them. The object counterexample uses an object of the partial limit itself, and the gauge argument proves nonextendibility up to equivalence, without adding a chosen identification of its homotopy group. Every set $G^q$ occurring here is finite. The examples therefore establish sharpness inside the same degreewise finite descent format as the recognition theorem. \end{remark} \section{A finite comparison criterion} \label{sec:comparison} The atlas theorem derives its mapping comparison from local sections. In other semantic presentations, one starts instead with a comparison functor and a component-lifting property. The following criterion separates that property from the presentations needed for objects. \subsection{From components to mapping spaces} We use the left exact full-faithfulness criterion of \cite[Lemma~13.3]{GambinoHenrySattlerSzumilo}. The proof below also records how conservativity supplies injectivity on components. The argument uses based loop objects in slices, so it retains the basepoint information needed to compare homotopy groups. \begin{lemma}[Components of the space of sections]\label{lem:section-components} Let $p:E\to A$ be a morphism in an $\infty$-category $\mathcal C$. Write \[ \operatorname{Sec}_{\mathcal C}(p) :=\operatorname{Map}_{\mathcal C_{/A}}(\operatorname{id}_A,p). \] Forgetting the specified homotopy $ps\simeq\operatorname{id}_A$ induces a natural bijection \[ \pi_0\operatorname{Sec}_{\mathcal C}(p) \;\xrightarrow{\ \sim\ }\; \bigl\{[s]\in\operatorname{Hom}_{h\mathcal C}(A,E) :[p][s]=[\operatorname{id}_A]\bigr\}. \] \end{lemma} \begin{proof} Put $G=\operatorname{Aut}_{\mathcal C}(A)$ and \[ T=\operatorname{Map}_{\mathcal C}(A,E) \mathbin{\times}_{\operatorname{Map}_{\mathcal C}(A,A)}G. \] Here $G$ is the union of the equivalence components in the endomorphism space. Composition gives a map over $G$ \[ \operatorname{Sec}_{\mathcal C}(p)\times G\longrightarrow T, \qquad (s,g)\longmapsto s\circ g, \] with the homotopy $p(sg)\simeq g$ induced by the section data. On the fibre over each $g\in G$, this is an equivalence: its inverse is precomposition with $g^{-1}$. Hence it is an equivalence of spaces over $G$. Since $T$ is the union of the components of $\operatorname{Map}_{\mathcal C}(A,E)$ whose composite with $p$ is an equivalence, the fibre over $[\operatorname{id}_A]$ of $\pi_0T\to\pi_0G$ is exactly the set on the right. The product description identifies this fibre with $\pi_0\operatorname{Sec}(p)$. \end{proof} \begin{lemma}[Passing to slices]\label{lem:homotopy-full-faithful-slices} Let $\mathcal C,\mathcal D$ admit pullbacks. Suppose that $F:\mathcal C\to\mathcal D$ preserves them and $hF:h\mathcal C\to h\mathcal D$ is fully faithful. Then, for every $B\in\mathcal C$, the induced functor \[ h(F_{/B}):h(\mathcal C_{/B})\longrightarrow h(\mathcal D_{/F B}) \] is fully faithful. \end{lemma} \begin{proof} For $a:A\to B$ and $e:E\to B$, there is a natural equivalence \[ \operatorname{Map}_{\mathcal C_{/B}}(a,e) \simeq \operatorname{Sec}_{\mathcal C}(A\times_B E\to A). \] Apply Lemma~\ref{lem:section-components}. Full faithfulness of $hF$ identifies the two ordinary hom-sets defining the section condition, and preservation of pullbacks identifies their pullback objects. It therefore induces a bijection on the displayed mapping spaces' sets of components. \end{proof} \begin{proposition}[Left exact full-faithfulness criterion] \label{prop:lex-full-faithfulness} Let $F:\mathcal C\to\mathcal D$ preserve finite limits, where $\mathcal C$ and $\mathcal D$ are $\infty$-categories with finite limits. The following are equivalent: \begin{enumerate} \item $F$ is fully faithful. \item $hF$ is fully faithful. \item $F$ is conservative and $hF$ is full. \end{enumerate} In particular, in (iii) no independent lifting or injectivity assumption on positive homotopy groups is required. \end{proposition} \begin{proof} The implications (i)$\Rightarrow$(ii)$\Rightarrow$(iii) hold for arbitrary $\infty$-functors. For (iii)$\Rightarrow$(ii), consider $f,g:A\to B$ with $Ff\simeq Fg$, and form the homotopy equalizer \[ p:E:=A\mathbin{\times}_{B\times B} B\longrightarrow A, \] where $A\to B\times B$ is $(f,g)$ and $B\to B\times B$ is the diagonal. The chosen homotopy gives a section $t:FA\to FE$ of $Fp$. Fullness of $hF$ supplies $s:A\to E$ with $Fs\simeq t$. Consequently $F(ps)\simeq\operatorname{id}_{FA}$. Conservativity implies that $ps$ is an equivalence. Replacing $s$ by $s(ps)^{-1}$ gives a section of $p$, and hence a homotopy $f\simeq g$. Thus $hF$ is faithful as well as full. It remains to prove (ii)$\Rightarrow$(i). Fix $A,B\in\mathcal C$ and a basepoint $f\in\operatorname{Map}_{\mathcal C}(A,B)$. In $\mathcal C_{/A}$, let $1_A=\operatorname{id}_A$, let $Q=(A\times B\to A)$, and point $Q$ by the section $\sigma_f=(\operatorname{id}_A,f):1_A\to Q$. Define $\Omega_{\sigma_f}Q=1_A\times_Q1_A$ in the slice, with its canonical pointing, and iterate this construction. Finite limits give natural equivalences, for every $k\ge1$, \[ \operatorname{Map}_{\mathcal C_{/A}} (1_A,\Omega_{\sigma_f}^{k}Q) \simeq \Omega_f^{k}\operatorname{Map}_{\mathcal C}(A,B). \] The functor $F_{/A}$ preserves these pointed loop objects. By Lemma~\ref{lem:homotopy-full-faithful-slices}, its homotopy-category functor is fully faithful. Taking components therefore gives \[ \pi_k(\operatorname{Map}_{\mathcal C}(A,B),f) \xrightarrow{\ \sim\ } \pi_k(\operatorname{Map}_{\mathcal D}(FA,FB),Ff) \qquad(k\ge1). \] Hypothesis (ii) already gives a bijection on $\pi_0$. Thus the map of mapping spaces is an equivalence, by the homotopy-group criterion for spaces. This holds for all $A,B$. \end{proof} \subsection{Effective presentations at a finite descent stage} Let $\X$ and $\Z$ be bounded coherent $\infty$-topoi and put \[ \C=\X^{\coh}_{\leq n},\qquad \D=\Z^{\coh}_{\leq n}. \] Suppose a cosimplicial diagram $\D^\bullet$ of locally $n$-truncated categories presents $\D$: \[ \D\simeq\lim_\Delta\D^\bullet. \] For a functor $e:\C\to\D$, write $e_q$ for its component in $\D^q$. For $A,B\in\C$, let \begin{equation}\label{eq:finite-semantic-map} T_{A,B}=\lim_{[q]\in\Delta_{\leq n+1}} \Map_{\D^q}(e_qA,e_qB). \end{equation} The compatible identifications in the cone defining $e$ are part of this diagram of mapping spaces. \begin{theorem}[Finite comparison by maps and presentations] \label{thm:finite-comparison} Assume that $e$ preserves finite limits, finite coproducts, and effective epimorphisms, and is conservative. Suppose: \begin{enumerate}[label=\textup{(\roman*)}] \item For all $A,B\in\C$, the natural map \[ \pi_0\Map_\C(A,B)\longrightarrow\pi_0T_{A,B} \] is surjective. \item Every $Y\in\D$ has an effective epimorphism $eU\to Y$ with $U\in\C$, whose kernel-pair object is equivalent to $eV$ for some $V\in\C$. \end{enumerate} Then $e$ is an equivalence. The semantic target can be computed through degree $n+2$, and the mapping test \textup{(i)} uses only degrees through $n+1$. \end{theorem} \begin{proof} Theorem~\ref{hr:thm-finite-descent} identifies $T_{A,B}$ with $\Map_\D(eA,eB)$. Thus (i) says that $he$ is full. Since $e$ is conservative and left exact, Proposition~\ref{prop:lex-full-faithfulness} shows that $e$ is fully faithful. Let $eU\to Y$ be a presentation in (ii). Its entire \v{C}ech nerve has terms in the essential image of $e$: all terms are finite iterated fibre products of $eU$ and $eV$. Full faithfulness therefore lifts the diagram, with its face maps, degeneracies, and coherences, to a groupoid object $R_\bullet$ of $\C$. The map $eV\to eU\times eU$ is a pullback of the diagonal of $Y$, so it is $(n-1)$-truncated. The iterated diagonal criterion and conservativity of $e$ imply that $R_1\to R_0\times R_0$ is $(n-1)$-truncated in $\C$. Lemma~\ref{lem:efficient-quotient} gives its effective quotient $Q\in\C$. The map $U\to Q$ is an effective epimorphism. Since $e$ preserves this epimorphism and its \v{C}ech nerve, $eQ$ is the effective quotient of $eR_\bullet$. The same nerve has quotient $Y$. Thus $eQ\simeq Y$. This proves essential surjectivity; the bound on the target follows from Theorem~\ref{hr:thm-finite-descent}. \end{proof} The object condition specifies only a covering object and its kernel-pair object. It does not postulate that the transition maps are definable. Those maps lift only after the mapping comparison has been proved. Likewise, a groupoid quotient is used only after its efficiency has been checked. These two steps are necessary when working at a fixed truncation level. \begin{example}[Conservativity does not supply the mapping test] For a nontrivial finite group $H$, the forgetful functor from finite $H$-sets to finite sets is conservative and preserves finite limits, finite coproducts, and effective epimorphisms. It is essentially surjective, by giving any finite set the trivial action. It is not full: a map from the one-point trivial $H$-set to the regular $H$-set cannot be equivariant. Thus conservativity cannot replace (i), even at $n=0$. \end{example} \section{The homotopy type detected by finite models} \label{sec:detected-type} For a $\pi$-finite space $X$ and $n\geq0$, write \[ \mathcal L_n(X)=\Fun(X,\Fn). \] Equivalently, this is the category of families over $X$ with $\pi$-finite $n$-truncated homotopy fibres. Truncation is relative to $X$. The total space of such a family need not be an $n$-type. \begin{lemma}[Dependence on the base truncation] \label{lem:base-truncation} For any space $X$, the truncation map induces an equivalence \[ \Fun(\tau_{\leq n+1}X,\Fn) \xrightarrow{\sim}\Fun(X,\Fn). \] More generally, the same assertion holds with $\Fn$ replaced by any locally $n$-truncated $\infty$-category. \end{lemma} \begin{proof} Let $\mathcal E$ be locally $n$-truncated. The $r$th space of its complete Segal nerve is $\Fun([r],\mathcal E)^\simeq$, an $(n+1)$-type. Exponential adjunction and the fact that $X$ is a groupoid identify the $r$th space of the complete Segal nerve of $\Fun(X,\mathcal E)$ with \[ \Map\bigl(X,\Fun([r],\mathcal E)^\simeq\bigr). \] Mapping into this $(n+1)$-type depends only on $\tau_{\leq n+1}X$. Thus the comparison is an equivalence at every level of the complete Segal nerve. \end{proof} \begin{theorem}[Finite higher Galois duality] \label{thm:finite-duality} Let $X,Y$ be $\pi$-finite $(n+1)$-types. Pullback gives an equivalence \begin{equation}\label{eq:finite-duality} \Map(Y,X)\xrightarrow{\sim} \Fun^{\mathrm{lex},\amalg,\mathrm{epi}} \bigl(\mathcal L_n(X),\mathcal L_n(Y)\bigr). \end{equation} The right side is the full category of functors preserving finite limits, finite coproducts, and effective epimorphisms, with all natural transformations. In particular, it is a groupoid. \end{theorem} \begin{proof} Proposition~\ref{hc:prop-converse} supplies the finite point atlas of $\mathcal L_n(X)$. Theorem~\ref{hr:thm-models} therefore gives \[ \Fun^{\mathrm{lex},\amalg,\mathrm{epi}} \bigl(\mathcal L_n(X),\Fn\bigr)\simeq X. \] Finite limits, finite coproducts, and effective epimorphisms in $\mathcal L_n(Y)$ are computed pointwise. Consequently exponential adjunction restricts to \begin{align*} \Fun^{\mathrm{lex},\amalg,\mathrm{epi}} \bigl(\mathcal L_n(X),\Fun(Y,\Fn)\bigr) &\simeq \Fun\bigl(Y, \Fun^{\mathrm{lex},\amalg,\mathrm{epi}} (\mathcal L_n(X),\Fn)\bigr)\\ &\simeq\Fun(Y,X). \end{align*} The last category is the mapping space $\Map(Y,X)$. Under these equivalences a map $f:Y\to X$ yields the family of models $y\mapsto\omega_{f(y)}$, which is precisely pullback by $f$. \end{proof} \begin{corollary}[Exact detection of the visible homotopy type] \label{cor:truncation-recognition} For a map $f:Y\to X$ between $\pi$-finite spaces, the following conditions are equivalent: \begin{enumerate}[label=\textup{(\roman*)}] \item $f^*:\mathcal L_n(X)\to\mathcal L_n(Y)$ is an equivalence; \item $\tau_{\leq n+1}f$ is an equivalence. \end{enumerate} Moreover, for every $\pi$-finite $X$, \[ \Mod_n(\mathcal L_n(X))\simeq\tau_{\leq n+1}X. \] \end{corollary} \begin{proof} Lemma~\ref{lem:base-truncation} reduces the question to $(n+1)$-types. For those types, precomposition by $f^*$ on model categories identifies with $f:Y\to X$, since it takes evaluation at $y$ to evaluation at $f(y)$. An equivalence $f^*$ induces an equivalence of these full model categories, proving (i)$\Rightarrow$(ii). The converse is immediate from the lemma. The model-space formula follows from the same reduction and Theorem~\ref{hr:thm-models}. \end{proof} This result concerns the entire finite model category, including its higher transformations. Taking only isomorphism classes of models, or replacing its mapping spaces by sets of components, can remove information inside the displayed $(n+1)$-type. The examples below locate that loss explicitly. \begin{remark}[The ambient topos need not be recovered] Take $\mathcal X=\Fun(K(A,n+2),\mathcal S)$ for a nonzero finite abelian group $A$. Lemma~\ref{lem:base-truncation} gives $\mathcal X^{\coh}_{\leq n}\simeq\mathcal F_n$, so the singleton atlas $P=1$ satisfies the theorem and its recovered model space is the point. In the ambient topos, however, the point object over $K(A,n+2)$ has fibre $K(A,n+1)$ and retains the group $A$. This object lies outside the fixed $n$-truncation range. To see directly that this topos differs from $\mathcal S$, put $K=K(A,n+2)$. Then $\Gamma_{\mathcal X}\Delta K\simeq\Map(K,K)$ has distinct components containing the zero and identity maps, whereas $\Gamma_{\mathcal S}\Delta K\simeq K$ is connected. The conclusion of the theorem therefore concerns the fixed range, not the whole topos. \end{remark} \section{The universal parameter of an exact functor} \label{sec:universal-parameter} Write $\Fun^{\mathrm{ex}}$ for functors preserving finite limits, finite coproducts, and effective epimorphisms. Throughout this section, $\C$ and $\D$ are categories satisfying the recognition theorem at the same level $n$. Thus \[ \C\simeq\mathcal L_n(X),\qquad \D\simeq\mathcal L_n(Y) \] for $\pi$-finite $(n+1)$-types $X$ and $Y$. The following result associates a single intrinsic parameter object to every exact functor. It also determines all its factorizations through a slice. For $A\in\C$, let \[ \pi_A^*:\C\longrightarrow\C/A, \qquad B\longmapsto(B\times A\longrightarrow A). \] The slice $\C/A$ again satisfies the recognition theorem: if $Z_A\to X$ is the finite $n$-truncated family represented by $A$, then $Z_A$ is a $\pi$-finite $(n+1)$-type and \begin{equation}\label{eq:slice-as-family-category} \C/A\simeq\mathcal L_n(Z_A). \end{equation} Indeed, a family with $n$-truncated fibres over $Z_A$ has $n$-truncated fibres over $X$, since $Z_A\to X$ is itself $n$-truncated. The converse follows by taking fibres of a map between $n$-types. \begin{lemma}[Finite relative left adjoints] \label{lem:finite-relative-left-adjoint} Every exact functor $F:\C\to\D$ admits a left adjoint $F_!$. This adjoint satisfies the projection formula \begin{equation}\label{eq:finite-projection-formula} F_!(B\times F(A))\simeq F_!(B)\times A, \qquad A\in\C,\ B\in\D. \end{equation} Put $P_F=F_!(1_\D)$. Under Theorem~\ref{thm:finite-duality}, if $F=f^*$ for $f:Y\to X$, then $P_F$ is the relative $n$-truncation of $Y\to X$: \begin{equation}\label{eq:relative-parameter-fibres} (P_F)_x\simeq\tau_{\leq n}\operatorname{hofib}_x(f). \end{equation} \end{lemma} \begin{proof} Use the equivalence $F\simeq f^*$ of Theorem~\ref{thm:finite-duality}. An object $B\in\mathcal L_n(Y)$ is a family $V\to Y$. Compose it with $f$ and take relative $n$-truncation over $X$. This gives $F_!B$. Its fibre over $x$ is \[ \tau_{\leq n}(V\times_X\{x\}). \] The space before truncation is $\pi$-finite: both the relevant base fibre and the fibres of $V\to Y$ are $\pi$-finite, and the assertion follows from the homotopy exact sequence. Hence the construction remains inside $\mathcal L_n(X)$. Composition of families is left adjoint to pullback in spaces, and relative truncation is left adjoint to the inclusion of $n$-truncated families. Their composite is therefore left adjoint to $f^*$ on these finite categories. On the fibre over $x$, the left side of \eqref{eq:finite-projection-formula} is \[ \tau_{\leq n}\bigl((V\times_X\{x\})\times A_x\bigr) \simeq\tau_{\leq n}(V\times_X\{x\})\times A_x. \] This equivalence uses preservation of finite products by truncation and $A_x\in\mathcal F_n$. It is natural in $x$, so proves the projection formula. Taking $B=1_\D$ gives \eqref{eq:relative-parameter-fibres}. \end{proof} Let $u_F:1_\D\to F(P_F)$ denote the unit of this adjunction at $1_\D$. For $A\in\C$, define the space of slice factorizations by \[ \mathcal R_A(F)= \operatorname{hofib}_{F}\left( \Fun^{\mathrm{ex}}(\C/A,\D) \xrightarrow{\,J\mapsto J\pi_A^*\,} \Fun^{\mathrm{ex}}(\C,\D)\right). \] Thus a point includes a specified equivalence $J\pi_A^*\simeq F$. The functor categories here are groupoids by finite higher Galois duality. \begin{theorem}[Universal parameter and exact slice factorization] \label{thm:universal-parameter} Let $F:\C\to\D$ be exact. \begin{enumerate}[label=\textup{(\roman*)}] \item The pair $(P_F,u_F)$ represents all parameters which acquire a chosen section after applying $F$: \begin{equation}\label{eq:all-parameter-factorizations} \mathcal R_A(F) \simeq\Map_\D(1_\D,F(A)) \simeq\Map_\C(P_F,A). \end{equation} For a section $a:1_\D\to F(A)$, the corresponding functor is \begin{equation}\label{eq:section-factor-functor} J_a(B\longrightarrow A)= 1_\D\mathbin{\times}_{F(A)}F(B). \end{equation} \item There is a canonical factorization \begin{equation}\label{eq:canonical-parameter-factor} \C\xrightarrow{\ \pi_{P_F}^*\ } \C/P_F\xrightarrow{\ J_F\ }\D, \qquad F\simeq J_F\pi_{P_F}^*, \end{equation} where $J_F=J_{u_F}$ is fully faithful and exact. More generally, $J_a$ is fully faithful if and only if the map $P_F\to A$ corresponding to $a$ is an equivalence. Consequently \eqref{eq:canonical-parameter-factor} is, up to contractible choice, the unique slice factorization whose second functor is fully faithful. \item The following conditions are equivalent: \begin{enumerate}[label=\textup{(\alph*)}] \item $F$ is fully faithful; \item $P_F\simeq1_\C$; \item $u_F$ is homotopic to $F(s)$ for a section $s:1_\C\to P_F$; \item for every $A\in\C$, every section of $F(A)$ is homotopic to the image of a section of $A$. \end{enumerate} Under these conditions the comparison of section spaces is an equivalence, including all higher homotopies. \item $F$ is conservative if and only if $P_F\to1_\C$ is an effective epimorphism. \end{enumerate} \end{theorem} \begin{proof} The second equivalence in \eqref{eq:all-parameter-factorizations} is adjunction. For the first, a factorization $J\pi_A^*\simeq F$ takes the diagonal \[ 1_{\C/A}\longrightarrow\pi_A^*A \] to a section $a:1_\D\to F(A)$. Every object $B\to A$ is the pullback in $\C/A$ of this diagonal along $\pi_A^*(B\to A)$. Left exactness therefore forces \eqref{eq:section-factor-functor}. Conversely, that formula defines an exact functor: finite limits are preserved, and finite coproducts and effective epimorphisms are stable under pullback. It comes with $J_a\pi_A^*\simeq F$. The two constructions are mutually inverse naturally in the section and in its higher homotopies; thus they give an equivalence of spaces, not just a bijection of components. For any exact functor $T$ between categories of the present form, Lemma~\ref{lem:finite-relative-left-adjoint} gives \[ T_!T(A)\simeq A\times T_!(1). \] The counit is the projection to $A$. A right adjoint is fully faithful precisely when its counit is an equivalence. Consequently \begin{equation}\label{eq:fullfaithful-terminal-parameter} T\text{ is fully faithful}\quad\Longleftrightarrow\quad T_!(1)\simeq1. \end{equation} For $J_a$, its left adjoint sends $D\in\D$ to $F_!D\to A$, where the structure map is adjoint to $D\to1_\D\xrightarrow{a}F(A)$. This follows directly by taking the fibre of the adjunction equivalence over the specified structure map. In particular, \[ (J_a)_!(1_\D)=(P_F\longrightarrow A) \quad\text{in }\C/A. \] By \eqref{eq:fullfaithful-terminal-parameter}, $J_a$ is fully faithful exactly when this object is terminal, equivalently when $P_F\to A$ is an equivalence. Taking $a=u_F$ gives the identity of $P_F$, and proves (ii). The space of equivalences out of a fixed object, with their targets allowed to vary, is contractible; this also gives the asserted uniqueness. The equivalence of (iii)(a) and (iii)(b) is \eqref{eq:fullfaithful-terminal-parameter}. If $u_F\simeq F(s)$, adjunction identifies this equality with \[ \id_{P_F}\simeq \bigl(P_F\longrightarrow1_\C\xrightarrow{s}P_F\bigr). \] Hence $P_F\to1_\C$ is an equivalence. Conversely, if $P_F\simeq1_\C$, adjunction identifies $\Map_\D(1,F(A))$ with $\Map_\C(1,A)$ naturally in $A$. This proves (iii)(b)$\Rightarrow$(iii)(d), including the assertion about higher section spaces. Applying (iii)(d) to $A=P_F$ and the distinguished section $u_F$ gives (iii)(c), completing the equivalence of the four conditions. Finally write $F=f^*$. It is conservative if $\pi_0(f)$ is surjective, since equivalences of families can then be tested over points in the image. If a component of $X$ is missed, the map of families which is $\varnothing\to *$ on that component and an equivalence on the others disproves conservativity. On the other hand, \eqref{eq:relative-parameter-fibres} says that $P_F\to1$ is an effective epimorphism exactly when every homotopy fibre of $f$ is nonempty. This is again surjectivity of $\pi_0(f)$. \end{proof} The parameter $P_F$ is initial among objects with a chosen $F$-section: the category of pairs $(A,a)$ is equivalent to the undercategory $\C_{P_F/}$. Part (iii) shows that the single distinguished section $u_F$ is a complete test for eliminating these relative parameters. Merely asking whether $P_F$ has some section would be weaker; the section must induce $u_F$ after applying $F$. The topological interpretation of \eqref{eq:canonical-parameter-factor} is the relative truncation factorization \begin{equation}\label{eq:connected-truncated-factor} Y\xrightarrow{q}Z\xrightarrow{p}X, \qquad Z=(\tau_{\leq n}^{X}Y)_{\mathrm{total}}. \end{equation} Here $p$ has $n$-truncated fibres and the fibres of $q$ have contractible $n$-truncations. In the convention that a space is $n$-connected when its $n$-truncation is contractible, the fibres of $q$ are $n$-connected. This is the standard connected--truncated factorization of spaces; see \cite[Sections~5.5.6 and~6.5.1]{LurieHTT}. The theorem identifies it entirely in terms of the exact functor and its possible parameter extensions. \begin{proposition}[Composition and change of parameters] \label{prop:universal-parameter-calculus} For exact functors $F:\C\to\D$ and $G:\D\to\mathcal E$, there is a natural equivalence \begin{equation}\label{eq:parameter-composition} P_{GF}\simeq F_!(P_G). \end{equation} For $A\in\C$, the induced exact functor $F_A:\C/A\to\D/F(A)$ has universal parameter \begin{equation}\label{eq:parameter-basechange} P_{F_A}\simeq(A\times P_F\longrightarrow A). \end{equation} Consequently full faithfulness can be checked after a finite effective-epimorphic parameter extension: if $A\to1$ is an effective epimorphism, then $F_A$ is fully faithful if and only if $F$ is fully faithful. \end{proposition} \begin{proof} The composite has left adjoint $F_!G_!$, which proves \eqref{eq:parameter-composition}. The left adjoint of $F_A$ sends $D\to F(A)$ to $F_!D\to A$, using the counit. On the terminal object this gives $F_!F(A)\to A$. The projection formula identifies it with $A\times P_F\to A$, proving \eqref{eq:parameter-basechange}. An equivalence between families is detected after pullback along an effective epimorphism. Apply this to $P_F\to1$ and use Theorem~\ref{thm:universal-parameter}(iii). \end{proof} \begin{corollary}[Finite descent from the universal parameter] \label{cor:universal-parameter-descent} For an exact functor $F:\C\to\D$, the following are equivalent: \begin{enumerate}[label=\textup{(\roman*)}] \item $F$ is conservative; \item $P_F\to1_\C$ is an effective epimorphism; \item restriction along the powers of $P_F$ induces an equivalence \begin{equation}\label{eq:universal-parameter-descent} \C\simeq \lim_{[q]\in\Delta_{\leq n+2}}\C/P_F^{q+1}. \end{equation} \end{enumerate} Mapping spaces between compatible objects in this limit are determined through degree $n+1$. Both degree bounds are optimal among conservative exact functors. \end{corollary} \begin{proof} The first equivalence is Theorem~\ref{thm:universal-parameter}. If $P_F$ covers $1$, let $Z\to X$ be its total family. The augmented \v{C}ech nerve of $Z\to X$ has colimit $X$ in spaces. Taking functor categories into $\mathcal F_n$ gives \[ \C\simeq\lim_\Delta\C/P_F^{q+1}. \] Here \eqref{eq:slice-as-family-category} identifies the individual terms. Theorem~\ref{hr:thm-finite-descent} gives the two finite cutoffs. If $P_F$ does not cover $1$, all its powers miss a component of $X$. The non-equivalence used in the proof of conservativity above becomes an equivalence in every slice term, so (iii) cannot hold. For sharpness, take the evaluation functor $\mathcal L_n(BC_2)\to\mathcal F_n$. Its universal parameter is the regular $C_2$-torsor, and the displayed diagram has terms $\mathcal F_n^{C_2^q}$. Thus Proposition~\ref{hs:prop-sharp-actions} supplies both strict lower bounds within this class. \end{proof} \begin{corollary}[Homotopy criterion for full faithfulness] \label{cor:fullfaithful-homotopy} Let $f:Y\to X$ be a map of $\pi$-finite $(n+1)$-types. The exact functor $f^*:\mathcal L_n(X)\to\mathcal L_n(Y)$ is fully faithful if and only if every homotopy fibre of $f$ is $n$-connected. Equivalently, $f$ is bijective on components, induces isomorphisms on $\pi_i$ for $1\leq i\leq n$, and induces surjections on $\pi_{n+1}$ at every base point. \end{corollary} \begin{proof} The first assertion follows from \eqref{eq:relative-parameter-fibres} and Theorem~\ref{thm:universal-parameter}(iii). The second is the homotopy exact sequence of each fibre. For $n=0$ it says precisely that $f$ is bijective on components and surjective on fundamental groups. \end{proof} \begin{example}[Finite group images] Let $\varphi:H\to G$ be a homomorphism of finite groups, and take $n=0$. Restriction $F:\operatorname{Fin}G\text{-}\mathrm{Set} \to\operatorname{Fin}H\text{-}\mathrm{Set}$ has \[ P_F=G/\im\varphi. \] Its canonical slice factorization is restriction to $\im\varphi$ followed by inflation along $H\twoheadrightarrow\im\varphi$. The latter is fully faithful. A parameter $A$ and a chosen $H$-fixed point of its restriction give a fully faithful slice factorization precisely when the induced map $G/\im\varphi\to A$ is an isomorphism. Thus the ordinary orbit parameter is the degree-zero instance of the universal parameter theorem. \end{example} \begin{example}[Higher image parameters] Let $n\geq1$, let $A,B$ be finite abelian groups, and let $\alpha:B\to A$. For the exact functor induced by \[ f=K(\alpha,n+1):K(B,n+1)\longrightarrow K(A,n+1), \] the universal parameter is the family \begin{equation}\label{eq:em-universal-parameter} K(\im\alpha,n+1)\longrightarrow K(A,n+1). \end{equation} Its fibre is $K(\coker\alpha,n)$. Indeed, the fibre of $f$ has $\pi_{n+1}=\ker\alpha$, $\pi_n=\coker\alpha$, and no other nonzero homotopy groups, while the factorization through $K(\im\alpha,n+1)$ has respectively $n$-connected and $n$-truncated fibres. In particular, $f^*$ is fully faithful exactly when $\alpha$ is surjective. For $B=0$ and $A\ne0$, the universal parameter has connected fibres $K(A,n)$, but it is not terminal. Thus replacing a higher parameter by its set of components can remove the complete obstruction to full faithfulness. Concretely, the family $*\to K(A,n+1)$ has no section, whereas its evaluation at the base point has sections. \end{example} \begin{proposition}[The first failure in a Postnikov projection] \label{prop:postnikov-detection-profile} Let $r\geq1$ and let $p:E\to B$ be a Postnikov projection from a connected $\pi$-finite $r$-type to its $(r-1)$-truncation. Assume $\pi_r(E)$ is nonzero. Then pullback has the following three regimes: \begin{center} \begin{tabular}{ll} \toprule Semantic level & Behaviour of $p^*$\\ \midrule $0\leq n\leq r-2$ & equivalence\\ $n=r-1$ & fully faithful and not essentially surjective\\ $n\geq r$ & conservative and not fully faithful\\ \bottomrule \end{tabular} \end{center} At the final range, the induced functor on homotopy categories is not full. The first range is empty when $r=1$. \end{proposition} \begin{proof} For $n\leq r-2$, the two bases have the same $(n+1)$-truncation, so Corollary~\ref{cor:truncation-recognition} applies. The fibres of $p$ are $K(\pi_r(E),r)$, with their natural monodromy. They have contractible $(r-1)$-truncations but noncontractible $r$-truncations. The universal-parameter criterion therefore gives full faithfulness precisely through level $r-1$. At level $r-1$ an equivalence would, by the same recognition corollary, force $p$ itself to be an equivalence, contrary to the nonzero top group. Conservativity holds at every level because $p$ is surjective on components. If the homotopy-category functor were full in the last range, the conservative left exact full-faithfulness criterion (Proposition~\ref{prop:lex-full-faithfulness}) would make $p^*$ fully faithful, a contradiction. \end{proof} \section{Relative Postnikov obstructions for exact functors} \label{sec:relative-postnikov} Finite higher Galois duality identifies a tower of semantic categories with the Postnikov tower of its model space. We now determine the obstruction to extending an exact functor by one level and the full space of extensions when that obstruction vanishes. The underlying classification of Eilenberg--Mac Lane fibrations and their section spaces is classical; see M\o ller~\cite[Theorem~3.1]{MollerSections} and M\o ller--Scherer~\cite[Lemma~2.1]{MollerSchererPostnikov}. Here it supplies intrinsic invariants of exact functors, including their relative natural automorphisms. \subsection{Local coefficients and affine maps} Let $B$ be a space and let $A:B\to\mathbf{Ab}_{\mathrm{fin}}$ be a local system of finite abelian groups. Thus $A$ factors through the fundamental groupoid of $B$, and transport acts by group isomorphisms. Write $K_B(A,q)\to B$ for its Eilenberg--Mac Lane family, with its zero section, and put \[ \mathcal H^q(B;A)=\Gamma_BK_B(A,q) =\Map_{\mathcal S/B}(B,K_B(A,q)). \] For $q\geq0$ this is an abelian group object in spaces. In particular, $\pi_0\mathcal H^q(B;A)=H^q(B;A)$, and \begin{equation}\label{eq:postnikov-section-homotopy} \pi_i\mathcal H^q(B;A)=H^{q-i}(B;A) \quad(0\leq i\leq q), \qquad \pi_i\mathcal H^q(B;A)=0\quad(i>q). \end{equation} The homotopy groups in positive degree are taken at the zero section. Translation gives the corresponding identifications at any other section. These formulas follow by looping the section space: limits commute with loops and $\Omega_B K_B(A,q)=K_B(A,q-1)$. A \emph{band identification} for a fibration with fibres $K(A_b,r)$ is a specified identification of the local system of $r$th homotopy groups with $A$. Band identifications will be retained unless their removal is stated explicitly. \begin{lemma}[Affine maps and banded extensions] \label{lem:postnikov-affine} Let $r\geq1$ and let $D,C$ be abelian groups. The map \begin{equation}\label{eq:affine-em-maps} K(C,r)\times\operatorname{Hom}(D,C) \longrightarrow\Map(K(D,r),K(C,r)),\qquad (c,\alpha)\longmapsto c+K(\alpha,r), \end{equation} is an equivalence. These equivalences respect composition in the form \[ (c,\alpha)\circ(d,\beta)=(c+\alpha(d),\alpha\beta). \] Consequently, for a local system $A$ on $B$, the space of fibrations over $B$ with Eilenberg--Mac Lane fibres in degree $r$ and band identification $A$ is \begin{equation}\label{eq:banded-extension-space} \mathcal H^{r+1}(B;A). \end{equation} It is equivalently the space of torsors under the group object $K_B(A,r)$ in $\mathcal S/B$. \end{lemma} \begin{proof} The pointed mapping space in~\eqref{eq:affine-em-maps} is discrete. Indeed, its components are \[ \widetilde H^r(K(D,r);C)=\operatorname{Hom}(D,C), \] by the Hurewicz theorem and the universal coefficient sequence. Its positive homotopy groups are the reduced cohomology groups in degrees below $r$, which vanish. Evaluation at the base point of $K(D,r)$ splits because the target is an abelian group object: subtracting that value makes a map pointed. This proves the equivalence. Choosing the functorial simplicial abelian models for $K(-,r)$ gives the displayed composition formula. In particular, the automorphism group object of $K(A,r)$ is $K(A,r)\rtimes\operatorname{Aut}(A)$. Its classifying space fits into the split fibration~\cite[Lemma~2.1]{MollerSchererPostnikov} \[ K(A,r+1)\longrightarrow B\operatorname{Aut}(K(A,r)) \longrightarrow B\operatorname{Aut}(A). \] Fixing the map $B\to B\operatorname{Aut}(A)$ that describes a local system leaves precisely the space of sections of its associated $K(A,r+1)$-family. This proves \eqref{eq:banded-extension-space}, component by component when the fibres of $A$ have different isomorphism types. The same description classifies $K_B(A,r)$-torsors: the universal torsor is the fibrewise path fibration from the zero section of $K_B(A,r+1)$. \end{proof} Choose a classifying section $\kappa\in\mathcal H^{r+1}(B;A)$. Its torsor can be represented as the family of paths from the zero section to $\kappa$. Thus its cohomology class is $[\kappa]\in H^{r+1}(B;A)$. Distinguishing a section from its cohomology class is necessary when the entire mapping space is to be retained. \subsection{The obstruction and the full space of lifts} Fix $r\geq2$, and let $X,Y$ be $\pi$-finite $r$-types. Put \[ B_X=\tau_{\leq r-1}X,\qquad B_Y=\tau_{\leq r-1}Y. \] The top homotopy groups give local systems $A_X$ on $B_X$ and $A_Y$ on $B_Y$. The Postnikov maps are banded torsors with classifying sections \[ \kappa_X\in\mathcal H^{r+1}(B_X;A_X),\qquad \kappa_Y\in\mathcal H^{r+1}(B_Y;A_Y). \] For a map $f:B_Y\to B_X$, let \[ \alpha:A_Y\longrightarrow f^*A_X \] be a homomorphism of local systems. It need not be invertible. The homomorphism $\alpha$ determines a pushforward of torsors, whose classifying section is $\alpha_*\kappa_Y$. Let $\mathsf D_r(Y,X)$ be the space of pairs $(f,\alpha)$. More precisely, it is the total space over $\Map(B_Y,B_X)$ with discrete fibre \[ \operatorname{Hom}_{\mathrm{LocAb}(B_Y)} (A_Y,f^*A_X) \] over $f$, with the transport induced by homotopies of $f$. Taking the lower Postnikov map and the top homotopy homomorphism defines \begin{equation}\label{eq:postnikov-data-map} \Map(Y,X)\longrightarrow\mathsf D_r(Y,X). \end{equation} Write $\mathsf{Lift}_r(f,\alpha)$ for its homotopy fibre over $(f,\alpha)$. A point of this fibre includes a map $Y\to X$ and the specified identification of its lower map with $f$. The lower semantic category is intrinsic: \[ \bigl(\mathcal L_{r-1}(X)\bigr)_{\leq r-2} =\mathcal L_{r-2}(X) \simeq\mathcal L_{r-2}(B_X). \] Indeed, the point objects of $X$ belong to $\mathcal L_{r-1}(X)$ and mapping out of them is evaluation. Thus internal truncation of an object is equivalent to pointwise truncation. A finite-limit-preserving functor preserves truncated objects, so restriction gives a map from the exact functor space in degree $r-1$ to that in degree $r-2$. Under Theorem~\ref{thm:finite-duality}, this restriction is precisely $\Map(Y,X)\to\Map(B_Y,B_X)$. Accordingly, $\mathsf{Lift}_r(f,\alpha)$ is also the space of exact functors \[ \mathcal L_{r-1}(X)\longrightarrow\mathcal L_{r-1}(Y) \] with a specified identification of their restriction with $f^*:\mathcal L_{r-2}(B_X)\to\mathcal L_{r-2}(B_Y)$ and specified induced homomorphism $\alpha$. \begin{theorem}[Relative Postnikov lifting for exact functors] \label{thm:relative-postnikov-lifts} With the preceding notation, there is an equivalence \begin{equation}\label{eq:postnikov-lift-path-space} \mathsf{Lift}_r(f,\alpha)\simeq \operatorname{Path}_{\mathcal H^{r+1}(B_Y;f^*A_X)} (\alpha_*\kappa_Y,f^*\kappa_X). \end{equation} It has the following consequences. \begin{enumerate}[label=\textup{(\roman*)}] \item A lift exists if and only if \begin{equation}\label{eq:relative-postnikov-obstruction} o_r(f,\alpha) =f^*[\kappa_X]-\alpha_*[\kappa_Y] =0\quad\text{in }H^{r+1}(B_Y;f^*A_X). \end{equation} \item When a lift exists, its entire space is a torsor for \begin{equation}\label{eq:postnikov-lift-torsor} \mathcal H^r(B_Y;f^*A_X). \end{equation} In particular, its components form a torsor for $H^r(B_Y;f^*A_X)$. At any chosen lift $L$, \begin{equation}\label{eq:postnikov-lift-homotopy} \pi_i(\mathsf{Lift}_r(f,\alpha),L) \cong H^{r-i}(B_Y;f^*A_X)\quad(1\leq i\leq r), \end{equation} and all higher homotopy groups vanish. \item The space of natural automorphisms of $L$ relative to the prescribed lower functor and band map is $\Omega_L\mathsf{Lift}_r(f,\alpha)$. Its components are $H^{r-1}(B_Y;f^*A_X)$ and its $j$th homotopy group is $H^{r-1-j}(B_Y;f^*A_X)$ for $1\leq j\leq r-1$. \end{enumerate} All these spaces are $\pi$-finite. The equivalences are natural in the Postnikov data and hence apply without choosing an atlas for the semantic categories. \end{theorem} \begin{proof} The homotopy fibre of $\Map(Y,X)\to\Map(B_Y,B_X)$ over $f$ is $\Map_{\mathcal S/B_Y}(Y,f^*X)$. Indeed, composition with $X\to B_X$ has target $\Map(Y,B_X)$, and the truncation universal property identifies this space with $\Map(B_Y,B_X)$. We must take the part inducing $\alpha$ on the top local systems. Regard $Y$ and $f^*X$ as torsors under $K_{B_Y}(A_Y,r)$ and $K_{B_Y}(f^*A_X,r)$, respectively. Every fibre map inducing $\alpha$ is, with a contractible space of choices, $K(\alpha,r)$-equivariant. To verify the assertion, trivialize the two torsors and their bands locally. It then becomes the equivalence~\eqref{eq:affine-em-maps} on the component labelled by $\alpha$. The affine composition formula shows that these equivalences respect the transition maps. Descent therefore identifies the full mapping spaces, including their higher homotopies. Extending the structure group along $K(\alpha,r)$ gives a $K_{B_Y}(f^*A_X,r)$-torsor $\alpha_*Y$. Equivariant maps from $Y$ to $f^*X$ identify with equivariant maps $\alpha_*Y\to f^*X$. Every such map is an equivalence of torsors. Their classifying sections are $\alpha_*\kappa_Y$ and $f^*\kappa_X$. The classification in Lemma~\ref{lem:postnikov-affine} now identifies the space of these equivalences with the path space in \eqref{eq:postnikov-lift-path-space}. A path exists exactly when its endpoints define the same component, proving~\eqref{eq:relative-postnikov-obstruction}. A nonempty path space in an abelian group object is a torsor for its loop space, and \[ \Omega\mathcal H^{r+1}(B_Y;f^*A_X) =\mathcal H^r(B_Y;f^*A_X). \] This proves the torsor assertion and all the homotopy-group formulas. The natural-automorphism assertion is the definition of the loop space of the relative functor groupoid. For finiteness, a $\pi$-finite space has a simplicial model with finitely many simplices in each degree. One constructs such models inductively using the finite bar construction for finite fundamental groups, the degreewise finite simplicial abelian models for $K(A,q)$, and their twisted path pullbacks. Normalized cochains with a finite local system are therefore finite in each degree, so each group in \eqref{eq:postnikov-lift-homotopy} is finite. The number of components is finite as well. Finally, the models of a recognized category recover $X$, its intrinsic truncation recovers $B_X$, and the homotopy groups and Postnikov class of this map recover $A_X$ and $[\kappa_X]$. Naturality of finite duality proves the last assertion. \end{proof} The theorem distinguishes three successive degrees: the obstruction lies in degree $r+1$, equivalence classes of relative lifts in degree $r$, and relative natural automorphisms in degree $r-1$. For $r=2$, these are respectively $H^3$, $H^2$, and $H^1$, while modifications of those natural automorphisms are recorded by $H^0$. \begin{corollary}[Fully faithful and invertible lifts] \label{cor:postnikov-faithful-lifts} If $o_r(f,\alpha)=0$, every lift with these data is fully faithful exactly when $f$ is an equivalence and $\alpha$ is surjective on every fibre. Every lift is an equivalence exactly when $f$ and $\alpha$ are equivalences. Hence the nonempty spaces of fully faithful lifts, and of equivalence lifts, have the entire torsor and automorphism structure of Theorem~\ref{thm:relative-postnikov-lifts}. \end{corollary} \begin{proof} By Corollary~\ref{cor:fullfaithful-homotopy}, pullback along a map of $r$-types is fully faithful at semantic level $r-1$ if and only if its homotopy fibres have contractible $(r-1)$-truncations. For $r$-types this is equivalent to an equivalence on their $(r-1)$-truncations and a surjection on their $r$th homotopy groups. These are exactly the two stated conditions. Equivalences of $r$-types are detected by the same lower equivalence and an isomorphism on the top homotopy groups; apply finite duality again. \end{proof} \begin{corollary}[Finite cochain description] \label{cor:postnikov-cochains} Choose a degreewise finite simplicial model for $B_Y$ and normalized cocycles representing the two Postnikov sections. Put $A=f^*A_X$ and $\delta=f^*\kappa_X-\alpha_*\kappa_Y\in Z^{r+1}(B_Y;A)$. The relative lift space is the space of cochain solutions \begin{equation}\label{eq:postnikov-cochain-solution} db=\delta,\qquad b\in C^r(B_Y;A), \end{equation} with all cochain homotopies retained. If a solution $b_0$ exists, translation by $b_0$ identifies this space with the Dold--Kan space of the nonnegative chain complex \begin{equation}\label{eq:postnikov-cochain-complex} D_i= \begin{cases} Z^r(B_Y;A),&i=0,\\ C^{r-i}(B_Y;A),&1\leq i\leq r,\\ 0,&i>r, \end{cases} \qquad \partial=d. \end{equation} Every group involved is finite. In particular, when the lift space is nonempty its homotopy cardinality is \begin{equation}\label{eq:postnikov-lift-cardinality} |\mathsf{Lift}_r(f,\alpha)| =\prod_{q=0}^{r}|H^q(B_Y;A)|^{(-1)^{r-q}}. \end{equation} \end{corollary} \begin{proof} Use the cocycle model for the local Eilenberg--Mac Lane family. A path between the classifying cocycles is a cochain $b$ as in~\eqref{eq:postnikov-cochain-solution}. A homotopy from $b$ to $b'$ is a cochain $c\in C^{r-1}$ with $dc=b'-b$; higher homotopies are given successively by cochains in degrees $r-2,\ldots,0$. This is precisely the Dold--Kan construction on the good truncation in~\eqref{eq:postnikov-cochain-complex}. Its homology is $H^{r-i}(B_Y;A)$ in degree $i$. The formula for homotopy cardinality is therefore the alternating product of the orders of the homotopy groups, including components. \end{proof} \subsection{Removing identifications and the first stage} \begin{proposition}[Homotopy transport of the lift space] \label{prop:postnikov-gauge} Let $d=(f,\alpha)$ and let $\mathsf D_r(Y,X)_d$ be its connected component. The space of exact functors whose Postnikov data lie in this component is \begin{equation}\label{eq:postnikov-gauge-quotient} \mathsf{Lift}_r(f,\alpha)\mathbin{\!//\!} \Omega_d\mathsf D_r(Y,X), \end{equation} where the action is homotopy transport in \eqref{eq:postnikov-data-map}. Its set of components is the orbit set of $\pi_0\mathsf{Lift}_r(f,\alpha)$ under $\pi_1(\mathsf D_r(Y,X),d)$. Assume that the lift space is nonempty. Suppose that a loop $\gamma$ in the data space has trivial coefficient transport, and choose the resulting identification of the pulled-back coefficient system on $B_Y\times S^1$ with the pullback of $A=f^*A_X$, restricting to the identity over $B_Y\times\{*\}$. Let $e_\gamma:B_Y\times S^1\to B_X$ be the corresponding evaluation map, and let $\alpha_\gamma$ be the corresponding band map on this product. Then its action on the torsor of components is translation by \begin{equation}\label{eq:postnikov-gauge-slant} \left(e_\gamma^*[\kappa_X] -(\alpha_\gamma)_*\operatorname{pr}_{B_Y}^*[\kappa_Y] \right)/[S^1] \in H^r(B_Y;A). \end{equation} The sign convention follows the path orientation from $\alpha_*\kappa_Y$ to $f^*\kappa_X$ in \eqref{eq:postnikov-lift-path-space}. \end{proposition} \begin{proof} A space over a connected base is the homotopy quotient of its homotopy fibre by the loop space of that base. Apply this fact to~\eqref{eq:postnikov-data-map}. Passing to components gives the orbit statement. For the final formula, transport a path from $\alpha_*\kappa_Y$ to $f^*\kappa_X$ around $\gamma$. Its endpoint differs from its starting point by the target endpoint loop minus the source endpoint loop. Under the loop--cohomology identification in \eqref{eq:postnikov-section-homotopy}, this difference is exactly slant product with the oriented circle. If coefficient transport is nontrivial, the same construction is an affine action whose linear part is that transport; a translation formula requires an identification of the coefficient systems. \end{proof} There is a different operation in which the band identification itself is forgotten. For a fixed base $B$ and an isomorphism class of local systems represented by $A$, the moduli space of Postnikov extensions with that unmarked band is \begin{equation}\label{eq:postnikov-band-quotient} \mathcal H^{r+1}(B;A)\mathbin{\!//\!} \operatorname{Aut}_{\mathrm{LocAb}(B)}(A). \end{equation} This follows directly from Lemma~\ref{lem:postnikov-affine}. It changes components by the action on cohomology and retains all stabilizers. In contrast, merely removing the chosen identification of a lower functor in~\eqref{eq:postnikov-gauge-quotient} does not remove the band identifications of the source and target. The restriction $r\geq2$ in Theorem~\ref{thm:relative-postnikov-lifts} is required for a general Postnikov tower: its first homotopy groups need not be abelian. The initial stage has a direct finite-groupoid description. Write \[ X_1=\coprod_{i\in I}BH_i,\qquad Y_1=\coprod_{j\in J}BG_j \] for finite sets $I,J$ and finite groups $H_i,G_j$. Then \begin{equation}\label{eq:first-stage-nonabelian} \Fun^{\mathrm{lex},\amalg,\mathrm{epi}} (\mathcal L_0(X_1),\mathcal L_0(Y_1)) \simeq \coprod_{\sigma:J\to I}\prod_{j\in J} \bigl(\operatorname{Hom}(G_j,H_{\sigma(j)}) \mathbin{\!//\!}H_{\sigma(j)}\bigr). \end{equation} Indeed, a functor of one-object groupoids is a group homomorphism and a natural transformation is an element conjugating one homomorphism to the other. The automorphism group at $\varphi:G\to H$ is $C_H(\varphi(G))$. This proves the mapping-space formula, and finite duality gives the semantic statement. No abelian cohomology formula is imposed on this first stage. \begin{corollary}[The finite tower of exact-functor lifts] \label{cor:finite-postnikov-tower} For $R\geq1$ and $\pi$-finite $R$-types $X,Y$, the full exact functor space $\Fun^{\mathrm{lex},\amalg,\mathrm{epi}} (\mathcal L_{R-1}(X),\mathcal L_{R-1}(Y))$ is obtained from \eqref{eq:first-stage-nonabelian} by $R-1$ successive applications of Theorem~\ref{thm:relative-postnikov-lifts}. At stage $r$, a chosen lower map $f_{r-1}:Y_{r-1}\to X_{r-1}$ and band map $\alpha_r$ have obstruction \[ f_{r-1}^*[\kappa_{X,r}] -(\alpha_r)_*[\kappa_{Y,r}] \in H^{r+1}(Y_{r-1};f_{r-1}^*\pi_rX), \] and a nonempty homotopy fibre is a torsor for $\mathcal H^r(Y_{r-1};f_{r-1}^*\pi_rX)$. The data spaces and their loop-space actions are retained at each step. \end{corollary} \begin{proof} Apply~\eqref{eq:postnikov-data-map} to the successive pairs $(\tau_{\leq r}Y,\tau_{\leq r}X)$ for $2\leq r\leq R$, and use finite duality at each stage. The final mapping space is $\Map(Y,X)$ because $X,Y$ are $R$-truncated. \end{proof} The construction is a tower of spaces. Its later obstruction classes depend on the lower lifts already chosen, and its transport actions account for identifications between those choices. A product of the cohomology groups alone would discard this dependence. \subsection{A twisted obstruction with a parity effect} Let $B=BC_2$, and let $A=\mathbb Z/4_{-}$ be the local system on which the nonidentity element acts by $a\mapsto-a$. Put $C=\mathbb F_2$ with trivial action. Reduction modulo $2$ defines a surjective homomorphism of local systems \[ q:A\longrightarrow C. \] The normalized $C_2$-cochain complex with coefficients in $A$ is \begin{equation}\label{eq:twisted-cyclic-cochains} \mathbb Z/4\xrightarrow{\,2\,}\mathbb Z/4 \xrightarrow{\,0\,}\mathbb Z/4 \xrightarrow{\,2\,}\mathbb Z/4 \xrightarrow{\,0\,}\cdots . \end{equation} To see the differentials directly, a normalized $d$-cochain is determined by its value on the tuple of $d$ nonidentity elements. Every middle term of its coboundary contains an identity argument and vanishes. The remaining coefficient is $-1+(-1)^{d+1}$, which is $2$ modulo $4$ for even $d$ and $0$ for odd $d$. Consequently, \[ H^0(B;A)=\{0,2\},\qquad H^{2j+1}(B;A)=A/2A\cong C_2,\qquad H^{2j+2}(B;A)=\{0,2\}\cong C_2. \] All differentials with coefficients in $C$ are zero. Reduction $q$ therefore induces an isomorphism in odd positive degrees and the zero map in even positive degrees. \begin{proposition}[Parity-dependent fully faithful lifting] \label{prop:twisted-postnikov-parity} For each $r\geq2$, let $Y_r\to B$ be the Postnikov extension with band $A$ and the nonzero class $[\kappa_Y]\in H^{r+1}(B;A)$. Let $X_r=B\times K(C,r)$, with its trivial Postnikov class and band $C$. Their lower semantic categories are both $\mathcal L_{r-2}(B)$. The identity functor on this lower category admits an exact lift \begin{equation}\label{eq:twisted-postnikov-functor} \mathcal L_{r-1}(X_r)\longrightarrow \mathcal L_{r-1}(Y_r) \end{equation} inducing $q$ on top homotopy groups if and only if $r$ is odd. Whenever such lifts exist, they are fully faithful, their marked equivalence classes form a two-element torsor, and at each lift \[ \pi_i\mathsf{Lift}_r(\mathrm{id}_B,q)=C_2 \quad(1\leq i\leq r). \] For even $r$ there is no fully faithful lift of the lower identity, even if the top band map is not prescribed. \end{proposition} \begin{proof} The obstruction is $-q_*[\kappa_Y]\in H^{r+1}(B;C)$. By \eqref{eq:twisted-cyclic-cochains}, it vanishes precisely when $r+1$ is even. For odd $r$, the lower map is the identity and the band map $q$ is surjective, so Corollary~\ref{cor:postnikov-faithful-lifts} gives full faithfulness. Since $H^d(BC_2;\mathbb F_2)=\mathbb F_2$ for every $d\geq0$, the lift-space formulas give exactly the asserted components and higher homotopy groups. Finally, $q$ is the only surjective homomorphism from $\mathbb Z/4_{-}$ to $\mathbb F_2$. Full faithfulness would force that homomorphism; for even $r$ its obstruction is nonzero. \end{proof} The spaces in the proposition are $\pi$-finite $r$-types. They have fundamental group $C_2$, top homotopy groups $\mathbb Z/4$ and $C_2$, and the indicated monodromy. Thus the parity obstruction concerns finite models and finite bands throughout. It arises one level above the common lower semantic category, and its vanishing controls the existence of a fully faithful functor at that next level. \section{Cyclic Postnikov families} \label{sec:cyclic-lifting} The relative lifting theorem gives a family in every higher degree for which existence, equivalence, and the loss of marked distinctions can all be calculated. Let $p$ be an odd prime and put $k=\mathbb F_p$. The usual periodic resolution of $C_p$, together with its cup product, gives \[ H^*(BC_p;k)=k[u]\otimes\Lambda(v),\qquad |v|=1,\quad |u|=2, \qquad u=\beta v. \] Here $\beta$ is the mod-$p$ Bockstein. For the ring calculation and its Bockstein description, see~\cite[Examples~3.41 and~3E.2]{HatcherAT}; the periodic resolution is recalled in~\cite[Example~3.2]{BrownLectures}. Define a nonzero class in every degree by \[ \xi_{2j}=u^j,\qquad \xi_{2j+1}=vu^j. \] For $r\geq2$ and $c\in k$, let $X_c^{(r)}$ be the $r$-type with Postnikov projection to $BC_p$, constant band $k$ in degree $r$, and invariant $c\xi_{r+1}$. Thus \[ X_c^{(r)}=\operatorname{hofib} \bigl(c\xi_{r+1}:BC_p\longrightarrow K(k,r+1)\bigr). \] The specified projection and the identification of its band are part of this notation. For $a,b\in k$, write $f_a:BC_p\to BC_p$ for the homomorphism $g\mapsto ag$ and $\alpha_b:k\to k$ for multiplication by $b$. Let $\mathcal L_{a,b}(c_Y,c_X)$ be the space of maps $X_{c_Y}^{(r)}\to X_{c_X}^{(r)}$ supplied with an identification of their lower map with $f_a$ and with prescribed band map $\alpha_b$. By Theorem~\ref{thm:finite-duality}, this is also the space of the corresponding marked exact functors \[ \mathcal L_{r-1}(X_{c_X}^{(r)}) \longrightarrow\mathcal L_{r-1}(X_{c_Y}^{(r)}). \] \begin{theorem}[Uniform cyclic lifting calculation] \label{thm:cyclic-lift-moduli} Put $e_r=\lceil(r+1)/2\rceil$. The space $\mathcal L_{a,b}(c_Y,c_X)$ is nonempty if and only if \begin{equation}\label{eq:cyclic-lift-equation} a^{e_r}c_X=b c_Y\quad\text{in }k. \end{equation} When nonempty, its set of components is a $k$-torsor and, at every point, \[ \pi_i\mathcal L_{a,b}(c_Y,c_X)\cong k\quad(1\leq i\leq r), \qquad \pi_i=0\quad(i>r). \] After choices there is an equivalence \begin{equation}\label{eq:cyclic-lift-space} \mathcal L_{a,b}(c_Y,c_X) \simeq\prod_{i=0}^{r}K(k,i). \end{equation} For $c_X=c_Y=1$, every $a\ne0$ permits exactly the band map $b=a^{e_r}$, and every resulting functor is an equivalence. \end{theorem} \begin{proof} Naturality of the Bockstein gives $f_a^*v=av$ and $f_a^*u=au$. Consequently $f_a^*\xi_{r+1}=a^{e_r}\xi_{r+1}$. The obstruction of Theorem~\ref{thm:relative-postnikov-lifts} is therefore $(a^{e_r}c_X-bc_Y)\xi_{r+1}$, which proves the criterion. The same theorem identifies a nonempty lift space as a torsor for $\Map(BC_p,K(k,r))$. Its homotopy groups are $H^{r-i}(BC_p;k)=k$ for $0\leq i\leq r$. For completeness, a connective chain complex presenting this mapping space is the truncation of the cochain complex $C^*(BC_p;k)$, with degrees reversed about $r$. A chain complex of vector spaces splits as its homology and a contractible complex. Dold--Kan then supplies the noncanonical product in~\eqref{eq:cyclic-lift-space}. If $a\ne0$ and $c_X=c_Y=1$, equation~\eqref{eq:cyclic-lift-equation} forces $b=a^{e_r}\ne0$. The induced maps on $\pi_1$ and $\pi_r$ are isomorphisms; these are all the nonzero homotopy groups. \end{proof} \subsection{The monodromy of the space of lifts} The $p$ marked components in the theorem need not remain distinct when the identification of the lower functor is forgotten. The band identifications on the source and target are kept fixed throughout. Let $\mathcal U_{a,b}(c_Y,c_X)$ denote the space of maps with induced homomorphisms $(a,b)$, without a specified homotopy identifying the lower map with the chosen representative $f_a$. There is a fibre sequence \begin{equation}\label{eq:cyclic-unmarked-fibration} \mathcal L_{a,b}(c_Y,c_X)\longrightarrow \mathcal U_{a,b}(c_Y,c_X)\longrightarrow \Map(BC_p,BC_p)_{f_a}\simeq BC_p. \end{equation} In particular, $\mathcal U$ is the homotopy quotient of the marked space by the loop group $C_p$ of the lower mapping component. \begin{proposition}[Parity of the gauge translation] \label{prop:cyclic-gauge} Assume~\eqref{eq:cyclic-lift-equation}. Under the path-transport convention that a loop of the target invariant adds its slant class, $t\in C_p=k$ acts on the torsor of marked components by translation by \[ \begin{cases} c_X a^{r/2}t\,u^{r/2},&r\text{ even},\\[2pt] 0,&r\text{ odd}. \end{cases} \] Thus, if $r$ is even and $c_Xa\ne0$, all $p$ marked components belong to one component of $\mathcal U$. If $r$ is odd, or if $r$ is even and $c_Xa=0$, $\mathcal U$ has $p$ components. Reversing the path-transport convention changes the displayed translation by a sign and leaves these orbit statements unchanged. \end{proposition} \begin{proof} A loop $t$ at $f_a$ is represented by the evaluation map $F_t:BC_p\times S^1\to BC_p$ whose induced homomorphism on fundamental groups is $(g,m)\mapsto ag+tm$. If $z$ denotes the generator of $H^1(S^1;k)$, then \[ F_t^*v=av+tz,\qquad F_t^*u=au. \] The second identity follows from $u=\beta v$ and $\beta z=0$. Transport in the path-space description of Theorem~\ref{thm:relative-postnikov-lifts} acts by the coefficient of $z$ in $F_t^*(c_X\xi_{r+1})$. For $r=2j$, this coefficient is $c_Xa^jt u^j$. For $r=2j-1$, the invariant is $c_Xu^j$, whose pullback has no $z$ term. This proves the formula. The components of the total space of~\eqref{eq:cyclic-unmarked-fibration} are precisely the orbits of this action on the components of its fibre. A nonzero translation homomorphism $k\to k$ is transitive; the zero homomorphism fixes every component. \end{proof} \begin{corollary}[The group of components of cyclic automorphisms] \label{cor:cyclic-automorphism-group} Let $p$ be odd, let $k=\mathbb F_p$, and let $X=X_1^{(r)}$ with $r\geq2$. The group of unmarked homotopy classes of self-equivalences is \begin{equation}\label{eq:cyclic-automorphism-group} \pi_0\Aut(X)\cong \begin{cases} k^\times,&r\text{ even},\\ k\times k^\times,&r\text{ odd}. \end{cases} \end{equation} The same groups are obtained from exact self-equivalences of $\mathcal L_{r-1}(X)$. In the odd case, the first factor is the group of vertical translations classified by $H^r(BC_p;k)$. \end{corollary} \begin{proof} A self-equivalence induces multiplication by some $a\in k^\times$ on $\pi_1(X)$ and by some $b\in k^\times$ on $\pi_r(X)$. Theorem~\ref{thm:cyclic-lift-moduli} forces $b=a^{e_r}$, and supplies such an equivalence for every $a$. Thus the induced action on the fundamental group defines a surjective group homomorphism \[ \rho:\pi_0\Aut(X)\longrightarrow k^\times. \] Its kernel consists of maps with lower and band maps both the identity, after forgetting the choice of a lower homotopy. Before that choice is forgotten, these components form $H^r(BC_p;k)$, with the identity self-map as zero. They are represented by fibrewise translations of the $K(k,r)$-torsor. Composition of translations adds their cohomology classes. If $r$ is even, Proposition~\ref{prop:cyclic-gauge} says that the lower loop group acts transitively on these marked components. Hence $\ker\rho$ is trivial, giving the first case of~\eqref{eq:cyclic-automorphism-group}. Suppose $r=2j-1$. The gauge action on components is trivial, so $\ker\rho=H^r(BC_p;k)\cong k$ as groups. Let $T$ be a self-equivalence with lower map $f_a$ and band map $\alpha_b$. Conjugating a vertical translation by $T$ changes its class $\gamma$ to \[ b\,(f_a^{-1})^*\gamma. \] This follows on each fibre from the affine formula: applying $T^{-1}$ changes the base by $f_a^{-1}$, and applying $T$ multiplies translation vectors by $b$. The group $H^r(BC_p;k)$ is generated by $vu^{j-1}$; $f_a^*$ acts on it by $a^j$, while $b=a^{e_r}=a^j$. The displayed conjugation is therefore the identity. We have obtained a central extension \[ 0\longrightarrow k\longrightarrow\pi_0\Aut(X) \xrightarrow{\rho}k^\times\longrightarrow1. \] It splits by an elementary coprime-order argument. Choose a generator of the cyclic group $k^\times$ and a lift $t$. Then $t^{p-1}$ lies in the central subgroup $k$. Since multiplication by $p-1$ is invertible on $k$, multiply $t$ by the unique element of $k$ which makes its $(p-1)$st power equal to the identity. The resulting lift generates a complement of order $p-1$, proving the second case of~\eqref{eq:cyclic-automorphism-group}. Finite higher Galois duality identifies self-equivalences of $X$ contravariantly with exact self-equivalences of its semantic category. Thus their component groups are opposite groups. The groups displayed above are abelian, so the same formulas hold for the semantic category. \end{proof} \begin{proposition}[Higher homotopy of unmarked cyclic lifts] \label{prop:cyclic-higher-gauge} Keep the source and target band identifications fixed, and suppose $(a,b)$ satisfies~\eqref{eq:cyclic-lift-equation}. Put $B=BC_p$ and $d=r+1$. There is a homotopy-fibre description \begin{equation}\label{eq:cyclic-gauge-homotopy-fibre} \mathcal U_{a,b}(c_Y,c_X) \simeq\operatorname{hofib}_0\left( \Psi_{a,b}:BC_p\longrightarrow\Map(B,K(k,d))_0\right). \end{equation} Here the subscript $0$ denotes the component of the zero cohomology class. If $\mu_a:B\times BC_p\to B$ is induced by $(g,t)\mapsto ag+t$, then $\Psi_{a,b}$ is adjoint to the class \begin{equation}\label{eq:cyclic-universal-gauge-class} c_X\mu_a^*\xi_d-bc_Y\operatorname{pr}_1^*\xi_d \in H^d(B\times BC_p;k). \end{equation} In particular: \begin{enumerate}[label=\textup{(\roman*)}] \item If $r$ is even and $c_Xa\ne0$, the entire unmarked lift space has a noncanonical equivalence \begin{equation}\label{eq:cyclic-even-unmarked-space} \mathcal U_{a,b}(c_Y,c_X) \simeq\prod_{i=1}^{r}K(k,i). \end{equation} \item If $r=2j-1$ is odd, so $j\geq2$, put $m=c_Xj a^{j-1}\in k$. At each point $L$ of the unmarked lift space, \begin{equation}\label{eq:cyclic-odd-unmarked-fundamental-group} \pi_1(\mathcal U_{a,b}(c_Y,c_X),L)\cong \begin{cases} C_{p^2},&m\ne0,\\ C_p\times C_p,&m=0. \end{cases} \end{equation} For $2\leq i\leq r$ its $i$th homotopy group is $k$, and all groups above $r$ vanish. \end{enumerate} Consequently the identity component of the self-equivalence space of $X=X_1^{(r)}$ has fundamental group \begin{equation}\label{eq:cyclic-aut-fundamental-group} \pi_1(\Aut(X),\id_X)\cong \begin{cases} C_p,&r\text{ even},\\ C_{p^2},&r\text{ odd and }p\nmid(r+1)/2,\\ C_p\times C_p,&r\text{ odd and }p\mid(r+1)/2. \end{cases} \end{equation} The same formula describes the group of homotopy classes of natural automorphisms of the identity exact functor of $\mathcal L_{r-1}(X)$. \end{proposition} \begin{proof} Over the component $\Map(B,B)_{f_a}\simeq BC_p$, the fixed band map is the constant homomorphism $\alpha_b$. The path-space description of relative lifts therefore gives a point of $\mathcal U$ by choosing a lower map $f$ in this component and a path from $bc_Y\xi_d$ to $f^*(c_X\xi_d)$ in $\Map(B,K(k,d))$. Subtracting the constant endpoint gives \eqref{eq:cyclic-gauge-homotopy-fibre}. The evaluation map on this entire mapping component is $\mu_a$, so its adjoint class is~\eqref{eq:cyclic-universal-gauge-class}. Compatibility makes the component in $H^d(B;k)$ zero, as required for the indicated target component. Choose a splitting in simplicial $k$-modules of the truncated cochain complex which presents this target. It gives a noncanonical equivalence \[ \Map(B,K(k,d))_0\simeq\prod_{i=1}^{d}K(k,i), \] where the coefficient of the $i$th factor is $H^{d-i}(B;k)$, identified with $k$ using $\xi_{d-i}$ (and $\xi_0=1$). The K\"unneth components of \eqref{eq:cyclic-universal-gauge-class} give the corresponding cohomology classes of $\Psi_{a,b}$. Thus the splitting of the coefficient space retains the coherent gauge action through these possibly nonzero coordinate maps. Write $u_s,v_s$ for the classes on the first, source copy of $B$, and $u_g,v_g$ for the classes on the gauge copy. Naturality gives \[ \mu_a^*v=a v_s+v_g,\qquad \mu_a^*u=a u_s+u_g. \] For $r=2j-1$, the universal class becomes \begin{equation}\label{eq:cyclic-odd-gauge-polynomial} c_X\sum_{\ell=1}^{j}\binom{j}{\ell} a^{j-\ell}u_s^{j-\ell}u_g^\ell. \end{equation} Hence all odd coordinates of $\Psi_{a,b}$ are null, and its coordinate in $K(k,2\ell)$ is represented by \begin{equation}\label{eq:cyclic-odd-gauge-coordinate} c_X\binom{j}{\ell}a^{j-\ell}u_g^\ell \in H^{2\ell}(BC_p;k). \end{equation} In particular its $K(k,1)$ coordinate is zero and its first potentially nonzero Postnikov coordinate is $m u_g\in H^2(BC_p;k)$. This last class determines the fundamental group of each component of its homotopy fibre. Indeed, after lifting to the universal cover of the coefficient space, passage to its $2$-truncation gives $K(k,2)$. Higher target coordinates do not change the fundamental group of the fibre. The coefficient space is an abelian group object, so its fundamental group acts trivially on higher homotopy groups; the class $m u_g$ is independent of the choices in this lifting and in the splitting. It classifies the central extension \[ 0\longrightarrow k\longrightarrow\pi_1(\mathcal U,L) \longrightarrow C_p\longrightarrow1. \] Using the carry cocycle for $u_g$, this group is represented on pairs $(x,s)\in\{0,\ldots,p-1\}\times k$ by \[ (x,s)(y,t)= \left(x+y\bmod p, s+t+m\left\lfloor\frac{x+y}{p}\right\rfloor\right). \] If $m=0$ it is $C_p\times C_p$. If $m\ne0$, the $p$th power of $(1,0)$ is $(0,m)$, so $(1,0)$ has order $p^2$ and the group is cyclic. This proves \eqref{eq:cyclic-odd-unmarked-fundamental-group}. For $r=2j$, the two sorts of coordinates obtained from $(a v_s+v_g)(a u_s+u_g)^j$ are \begin{align*} \Psi_{2\ell}&: c_X\binom{j}{\ell}a^{j-\ell+1}u_g^\ell, &&1\leq\ell\leq j,\\ \Psi_{2\ell+1}&: c_X\binom{j}{\ell}a^{j-\ell}v_g u_g^\ell, &&0\leq\ell\leq j. \end{align*} In particular, $\Psi_1$ is the map $BC_p\to K(k,1)$ given by multiplication by $c_Xa^j$. Under the assumption of (i) this is an equivalence. For any map $(h,g):T\to T'\times W$ with $h$ an equivalence and $W$ connected, its homotopy fibre at a chosen point is equivalent to $\Omega W$. Applying this with $W=\prod_{i=2}^{r+1}K(k,i)$ proves \eqref{eq:cyclic-even-unmarked-space}. The higher homotopy groups in (ii) follow directly from \eqref{eq:cyclic-gauge-homotopy-fibre}, since the domain is a $1$-type and the target has $\pi_{i+1}=H^{r-i}(B;k)=k$ for $2\leq i\leq r$. For self-equivalences, take $c_X=c_Y=1$ and $a=b=1$. Then $m=j$, which gives~\eqref{eq:cyclic-aut-fundamental-group}. Finally the mapping-space equivalence in finite higher Galois duality takes the identity map to the identity exact functor and identifies their based loop spaces. \end{proof} \begin{corollary}[The homotopy type of a cyclic automorphism component] \label{cor:cyclic-padic-component} Let $p$ be odd, $k=\mathbb F_p$, and $r=2j-1\geq3$. Write $j=p^s q$ with $p\nmid q$, and put $h=2p^s-1$. Define the connected space \[ E_s= \begin{cases} BC_{p^2},&s=0,\\ X_1^{(h)},&s\geq1. \end{cases} \] For $X=X_1^{(r)}$, there is a noncanonical equivalence \begin{equation}\label{eq:cyclic-padic-component} \Aut(X)_{\id_X}\simeq E_s\times \prod_{\substack{1\leq i\leq r\\i\ne h}}K(k,i). \end{equation} More generally, for every $a\in k^\times$, the full unmarked lift space with compatible band map $b=a^j$ is \[ \mathcal U_{a,a^j}(1,1)\simeq k\times E_s\times \prod_{\substack{1\leq i\leq r\\i\ne h}}K(k,i), \] where the first factor is discrete. These are equivalences of spaces; no splitting of the composition law is asserted. \end{corollary} \begin{proof} In characteristic $p$, the odd-degree gauge polynomial satisfies \[ (a u_s+u_g)^j-a^j u_s^j =\sum_{\ell=1}^{q}\binom q\ell a^{j-p^s\ell}u_s^{j-p^s\ell}u_g^{p^s\ell}. \] Thus its first nonzero coordinate is in $K(k,2p^s)$ and is represented by \[ \lambda u_g^{p^s},\qquad \lambda=q a^{j-p^s}\ne0. \] Every remaining nonzero coordinate is a scalar multiple of a power of $u_g^{p^s}$. The $K(k,1)$ coordinate is zero, so its loop factor contributes the discrete copy of $k$. Put $E=\operatorname{hofib}(\lambda u^{p^s})$ for the map $BC_p\to K(k,2p^s)$. Split this coordinate off from the product model of $\Map(BC_p,K(k,r+1))_0$. The remaining fibre calculation is the homotopy fibre of a map \[ E\longrightarrow W=\prod_{\substack{2\leq t\leq r+1\\t\ne2p^s}}K(k,t). \] The class $u^{p^s}$ pulls back to zero on $E$, since $\lambda$ is invertible and $\lambda u^{p^s}$ has its tautological nullhomotopy there. Therefore every coordinate of this map to $W$ is null. The target is a finite product of Eilenberg--Mac Lane spaces, so choosing these nullhomotopies gives a nullhomotopy of the whole map. Its fibre is consequently $E\times\Omega W$. If $s=0$, the space $E$ is the classifying space of the nontrivial central extension of $C_p$ by $k$, hence $E\simeq BC_{p^2}$. If $s\geq1$, rescaling the coefficient group identifies $E$ with $X_1^{(h)}$. This proves the formula for the full unmarked lift space. Set $a=1$ and take its component containing the identity to obtain \eqref{eq:cyclic-padic-component}. \end{proof} \begin{example}[The degree $2p-1$ retains the original Postnikov class] \label{ex:cyclic-gauge-frobenius} Put $r=2p-1$ and $X=X_1^{(r)}$. For every $a\in k^\times$ the compatible band map is $b=a^p=a$. In \eqref{eq:cyclic-odd-gauge-polynomial}, all intermediate binomial coefficients vanish in $k$. Thus the only nonzero coordinate of $\Psi_{a,b}$ is the top coordinate $u_g^p\in H^{2p}(BC_p;k)$. The homotopy-fibre description therefore gives a noncanonical equivalence \[ \mathcal U_{a,a}(1,1) \simeq k\times X\times \prod_{i=1}^{2p-2}K(k,i), \] where the first factor is discrete. In particular, \[ \Aut(X)_{\id_X}\simeq X\times\prod_{i=1}^{2p-2}K(k,i). \] The original nonzero Postnikov class $u^p$ thus occurs inside the identity component of the exact self-equivalence space of $\mathcal L_{2p-2}(X)$, while its fundamental group is the split group $C_p\times C_p$. \end{example} The calculation distinguishes three pieces of data: the lower exact functor, the homomorphism of bands, and the chosen coherence between Postnikov classes. The first two determine existence through \eqref{eq:cyclic-lift-equation}; the third has a full $r$-type of choices. Forgetting a lower marking can identify distinct choices by the explicit action of Proposition~\ref{prop:cyclic-gauge}. \subsection{Finite cochain representatives} These examples have normalized finite representatives. Write elements of $C_p$ as integers in $\{0,\ldots,p-1\}$ and set \[ v(g)=g\bmod p,\qquad u(g,h)=\left\lfloor\frac{g+h}{p}\right\rfloor\bmod p. \] The identity $du=0$ expresses the independence of carries from the parenthesization of three summands. The connecting homomorphism obtained by lifting $v$ to $\mathbb Z/p^2$ gives this $u$, so it represents $\beta v$. Cup products of these cochains represent the classes $\xi_j$. For example, the $r=2$ invariant is \[ \kappa_c(g,h,\ell) =cg\left\lfloor\frac{h+\ell}{p}\right\rfloor\bmod p. \] The supplementary script \texttt{verify\_relative\_examples.py} checks cocycle identities, nontriviality, and the lift equation by exact row reduction in small normalized bar complexes. Its checked primes and degrees are recorded with the output. The periodic resolution and the proofs above establish the formulas in every degree. \section{Continuous semantics and uniform finite parameters} \label{pf:section} Let $n\geq0$ and let \[ P=\{P_i\}_{i\in I}\in \operatorname{Pro}(\Sps_{\pi,\leq n+1}) \] be a cofiltered system of $\pi$-finite $(n+1)$-types. Its category of continuous finite $n$-type families is \begin{equation}\label{pf:eq-continuous-families} \mathcal C_n(P)=\colim_{i\in I^{\op}}\mathcal L_n(P_i). \end{equation} The transition functors are pullbacks, and the colimit is taken in $\operatorname{Cat}_\infty$. In particular, an object is represented at a finite stage, while maps and their homotopies are identified after passage to a common later stage. Write \[ \operatorname{mat}(P)=\lim_{i\in I}P_i \] for the materialization in spaces. The continuous family category depends on the pro-object, and not on its chosen presentation. We continue to call a functor exact when it preserves finite limits, finite coproducts, and effective epimorphisms. We use two established facts about Stone $\infty$-topoi: the functor \[ P\longmapsto\mathcal X_P =\lim_i\Fun(P_i,\Sps), \] with the limit taken in the $\infty$-category of $\infty$-topoi and geometric morphisms, is fully faithful on profinite spaces, and materialization on profinite spaces is conservative \cite[Theorems~4.4.3 and~4.4.8]{BGHExodromy}. The fixed truncation range permits a direct comparison between continuous exact functors and these geometric morphisms. \begin{lemma}[A coherent site in the fixed range] \label{pf:lem-site} The $\infty$-topos $\mathcal X_P$ is bounded coherent and $(n+1)$-localic. There are natural equivalences \begin{equation}\label{pf:eq-site} \mathcal C_n(P)\simeq(\mathcal X_P)^{\coh}_{\leq n}, \qquad \operatorname{Sh}_{\mathrm{eff}}(\mathcal C_n(P)) \simeq\mathcal X_P, \end{equation} where the topology is generated by finite jointly effective epimorphic families. \end{lemma} \begin{proof} Each $\Fun(P_i,\Sps)\simeq\Sps/P_i$ is bounded coherent. Continuity for coherent objects gives \[ (\mathcal X_P)^{\coh}_{<\infty} \simeq\colim_i\Fun(P_i,\Sps_\pi); \] see~\cite[Propositions~3.9.1--3.9.2]{BGHExodromy}. This equivalence restricts to the $n$-truncated objects. Indeed, truncatedness is expressed by a finite iteration of diagonals ending in an equivalence. Finite limits commute with the displayed filtered colimit, and an equivalence in a filtered colimit is witnessed at a later stage. An object that becomes $n$-truncated therefore has an $n$-truncated representative after refinement. This proves the first equivalence in \eqref{pf:eq-site}. The $\infty$-topos $\Sps/P_i$ is $(n+1)$-localic because $P_i$ is an $(n+1)$-type. The inclusion of $(n+1)$-localic $\infty$-topoi preserves limits, so $\mathcal X_P$ is also $(n+1)$-localic; these facts are recalled in \cite[Paragraph~3.2.3 and Example~3.2.8]{BGHExodromy}. To verify the site assertion, let $A$ be a truncated coherent object of $\mathcal X_P$ and represent it by a finite family $A_i\to P_i$. Its total space is $\pi$-finite. Choose one point in each component of this total space. The resulting finite effective cover of $A_i$ has domains of the form $(*\to P_i)$. Their homotopy fibres are path spaces in $P_i$, and hence are $n$-truncated. Pulling the cover to $\mathcal X_P$ gives a finite cover of $A$ by objects of $\mathcal C_n(P)$. Thus $\mathcal C_n(P)$ is a basis for the effective-epimorphism topology on $(\mathcal X_P)^{\coh}_{<\infty}$. It is closed under finite limits and is locally $n$-truncated. The associated sheaf $\infty$-topos is therefore $(n+1)$-localic. The basis comparison in this fixed localic range gives the second equivalence in~\eqref{pf:eq-site}; see \cite[Corollary~3.12.14]{BGHExodromy}. \end{proof} \begin{theorem}[Continuous duality in a finite homotopy range] \label{pf:thm-duality} Let $P,Q\in\operatorname{Pro}(\Sps_{\pi,\leq n+1})$. Pullback induces an equivalence \begin{equation}\label{pf:eq-duality} \Map_{\operatorname{Pro}(\Sps_{\pi,\leq n+1})}(P,Q) \simeq \Fun^{\mathrm{lex},\amalg,\mathrm{epi}} \bigl(\mathcal C_n(Q),\mathcal C_n(P)\bigr). \end{equation} The right side contains all natural transformations; every one of them is invertible. In particular, \begin{equation}\label{pf:eq-models} \Mod_n(\mathcal C_n(P))\simeq\operatorname{mat}(P). \end{equation} For a pro-morphism $f:P\to Q$, the following conditions are equivalent: $f$ is an equivalence; $f^*$ is an equivalence; and the induced map on the complete spaces of finite models is an equivalence. \end{theorem} \begin{proof} Let $H:\mathcal C_n(Q)\to\mathcal C_n(P)$ be exact. Compose with the inclusion into $\mathcal X_P$. Since the source has finite limits, the colimit-preserving extension from its presheaf category is left exact \cite[Proposition~6.1.5.2]{LurieHTT}. Preservation of finite coproducts and effective epimorphisms says that $H$ carries every covering family to a covering family. Its extension therefore factors through the sheaf category in Lemma~\ref{pf:lem-site}, giving an inverse-image functor \[ \widetilde H:\mathcal X_Q\longrightarrow\mathcal X_P. \] This extension is unique, with its entire space of natural transformations, since the site objects generate the sheaf category under colimits. Conversely, every geometric morphism $\mathcal X_P\to\mathcal X_Q$ is coherent because its target is Stone~\cite[Corollary~4.4.15]{BGHExodromy}. Its inverse-image functor consequently restricts to an exact functor on the coherent $n$-truncated objects. The two constructions are inverse. Stone duality identifies these geometric morphisms with $\Map(P,Q)$, and their natural transformations are invertible \cite[Proposition~4.4.6]{BGHExodromy}. This proves \eqref{pf:eq-duality}. Take the source prospace to be the point, so that its family category is $\Fn$. Then \[ \Mod_n(\mathcal C_n(P)) \simeq\Map_{\operatorname{Pro}(\Sps_\pi)}(*,P) \simeq\lim_iP_i, \] which proves~\eqref{pf:eq-models}. Under this identification, precomposition with $f^*$ induces $\operatorname{mat}(f)$. An equivalence $f^*$ therefore gives an equivalence $\operatorname{mat}(f)$; profinite Whitehead then implies that $f$ is an equivalence. The other implications follow from pullback and~\eqref{pf:eq-models}. \end{proof} The duality in Theorem~\ref{pf:thm-duality} is the fixed-range form of higher Stone duality. Its use here is to give an exact boundary for the uniform parameter condition in Theorem~\ref{hr:thm-atlas}. \begin{corollary}[Finite-stage descent for exact functors and lifts] \label{pf:cor-certificates} For a $\pi$-finite $(n+1)$-type $X$ and a prospace $P=\{P_i\}_i$ as above, the natural comparison \begin{equation}\label{pf:eq-compact-functors} \colim_i \Fun^{\mathrm{lex},\amalg,\mathrm{epi}} (\mathcal L_n(X),\mathcal L_n(P_i)) \longrightarrow \Fun^{\mathrm{lex},\amalg,\mathrm{epi}} (\mathcal L_n(X),\mathcal C_n(P)) \end{equation} is an equivalence of spaces. More generally, let $u:X\to B$ be a map of $\pi$-finite $(n+1)$-types. Let $F:\mathcal L_n(B)\to\mathcal C_n(P)$ be exact, represented by $F_i$ at a finite stage $P_i$. Let $\operatorname{Lift}_F(u^*)$ denote the space of pairs $(H,\eta)$, where $H$ is exact and \[ H:\mathcal L_n(X)\to\mathcal C_n(P), \qquad \eta:H\circ u^*\simeq F. \] Write $F_j$ for the pullback of $F_i$ to $P_j$. Then \begin{equation}\label{pf:eq-compact-lifts} \operatorname{Lift}_F(u^*) \simeq \colim_{(j\to i)\in(I_{/i})^{\op}} \operatorname{Lift}_{F_j}(u^*). \end{equation} Consequently an extension exists precisely when it exists after one finite-stage refinement. Each specified equivalence or higher homotopy between such extensions also descends after refinement. \end{corollary} \begin{proof} By Theorem~\ref{pf:thm-duality}, the right side of \eqref{pf:eq-compact-functors} is $\Map(P,X)$. The defining mapping formula for pro-objects identifies it with $\colim_i\Map(P_i,X)$. Theorem~\ref{thm:finite-duality} identifies each term with the corresponding exact-functor space, proving~\eqref{pf:eq-compact-functors}. The chosen representation of $F$ corresponds to a map $f_i:P_i\to B$. Replace the index category by $I_{/i}$. The extension space is the homotopy fibre at the induced map $f:P\to B$ of \[ \Map(P,X)\longrightarrow\Map(P,B). \] Apply the pro-mapping formula to both terms. Filtered colimits of spaces commute with finite limits, so taking this fibre gives the filtered colimit of the fibres over $f_i|_{P_j}$. These are exactly the finite-stage extension spaces in~\eqref{pf:eq-compact-lifts}. \end{proof} \begin{corollary}[Continuous obstruction and the space of sections] \label{pf:cor-continuous-obstruction} Let $1\leq r\leq n+1$, let $B$ be a $\pi$-finite $(n+1)$-type, and let $A$ be a local system of finite abelian groups on $B$. Let $u:X\to B$ be a torsor under $K_B(A,r)$, with class $[\kappa]\in H^{r+1}(B;A)$. Thus $X$ is also a $\pi$-finite $(n+1)$-type. Let $F:\mathcal L_n(B)\to\mathcal C_n(P)$ correspond to $f:P\to B$, represented by $f_i:P_i\to B$. Write $f_j:P_j\to B$ for its pullback to a refinement $j\to i$, and define \begin{equation}\label{pf:eq-continuous-cohomology} H^q_{\mathrm{cont}}(P;f^*A) =\colim_{(j\to i)\in(I_{/i})^{\op}} H^q(P_j;f_j^*A)\qquad(q\geq0). \end{equation} The obstruction to extending $F$ along $u^*:\mathcal L_n(B)\to\mathcal L_n(X)$ is \begin{equation}\label{pf:eq-continuous-obstruction} o(F,u)=[f_i^*\kappa]_{\mathrm{cont}} \in H^{r+1}_{\mathrm{cont}}(P;f^*A). \end{equation} The extension space is nonempty if and only if $o(F,u)=0$, and this is equivalent to $f_j^*[\kappa]=0$ at some finite-stage refinement $j\to i$. When nonempty, the full extension space $\operatorname{Lift}_F(u^*)$ is a torsor under the abelian group object \begin{equation}\label{pf:eq-continuous-lift-group} \mathcal H^r_{\mathrm{cont}}(P;f^*A) =\colim_{(j\to i)\in(I_{/i})^{\op}} \Gamma_{P_j}K_{P_j}(f_j^*A,r). \end{equation} Its components form a torsor for $H^r_{\mathrm{cont}}(P;f^*A)$, and at any chosen extension $L$, \begin{equation}\label{pf:eq-continuous-lift-homotopy} \pi_\ell(\operatorname{Lift}_F(u^*),L) \cong H^{r-\ell}_{\mathrm{cont}}(P;f^*A) \quad(1\leq\ell\leq r), \qquad \pi_\ell=0\quad(\ell>r). \end{equation} No $(r-1)$-truncation hypothesis is imposed on the source stages $P_j$. \end{corollary} \begin{proof} At a finite stage $P_j$, the lift space is the space of sections of $f_j^*X\to P_j$. The classification of banded Eilenberg--Mac Lane torsors in Lemma~\ref{lem:postnikov-affine} identifies this space with the path space from the zero section to $f_j^*\kappa$ in $\Gamma_{P_j}K_{P_j}(f_j^*A,r+1)$. It is nonempty precisely when $f_j^*[\kappa]=0$; when nonempty it is a torsor for $\Gamma_{P_j}K_{P_j}(f_j^*A,r)$. Corollary~\ref{pf:cor-certificates} expresses the continuous extension space as the filtered colimit of these section spaces. A class is zero in the filtered colimit of the cohomology groups precisely when it is zero after some refinement. This proves the obstruction criterion. If a section exists at one stage, pull it back over the cofinal system of subsequent refinements. Translation by these compatible sections identifies the lift spaces with their section group objects. Taking the filtered colimit gives the torsor in~\eqref{pf:eq-continuous-lift-group}. Filtered colimits of spaces commute with finite limits and homotopy groups. Since \[ \pi_\ell\Gamma_{P_j}K_{P_j}(f_j^*A,r) =H^{r-\ell}(P_j;f_j^*A) \qquad(0\leq\ell\leq r), \] the component assertion and~\eqref{pf:eq-continuous-lift-homotopy} follow. This argument concerns sections of the target torsor over the full source $P_j$, so it applies in every source truncation degree allowed above. \end{proof} \begin{theorem}[Uniform finite parameter criterion] \label{pf:thm-uniform} For $P\in\operatorname{Pro}(\Sps_{\pi,\leq n+1})$, the following conditions are equivalent. \begin{enumerate} \item There are finitely many noninitial $U_a\in\mathcal C_n(P)$ covering the terminal object such that every object of $\mathcal C_n(P)/U_a$ has an effective epimorphism from a finite coproduct of copies of $U_a$. \item $\Mod_n(\mathcal C_n(P))$ is $\pi$-finite. \item $P$ is equivalent to the constant pro-object associated to a $\pi$-finite $(n+1)$-type $M$. \item $\mathcal C_n(P)\simeq\mathcal L_n(M)$ for such an $M$. \end{enumerate} If these conditions hold, $M$ is canonically identified with the complete finite model space of $\mathcal C_n(P)$. For arbitrary $P$, every finite family of objects of $\mathcal C_n(P)$ becomes constant on some finite coherent cover of the terminal object. \end{theorem} \begin{proof} Lemma~\ref{pf:lem-site} places $\mathcal C_n(P)$ in the setting of Theorem~\ref{hr:thm-atlas}. That theorem and Theorem~\ref{hr:thm-models} show that (i) implies (ii). Suppose (ii) holds, and put $M=\operatorname{mat}(P)$ using~\eqref{pf:eq-models}. As a limit of $(n+1)$-types, $M$ is an $(n+1)$-type. By assumption it is $\pi$-finite. The limit cone determines a canonical morphism of profinite spaces \[ \varepsilon:\operatorname{const}(M)\longrightarrow P. \] Its materialization is the identity of $M$: under $\Map(\operatorname{const}(M),P)\simeq \Map(M,\operatorname{mat}(P))$, the morphism $\varepsilon$ corresponds to $\id_M$. The conservative materialization functor therefore makes $\varepsilon$ an equivalence. This proves (iii). Condition (iii) immediately implies (iv), and Proposition~\ref{hc:prop-converse} gives (iv)$\Rightarrow$(i). The assertion about $M$ follows from the same construction. The empty case is included by allowing an empty covering family. Finally, represent any given finite family of objects at one stage $P_i$. Choose one point in each component of $P_i$ and pull its point atlas back to $\mathcal X_P$. Over each member of this finite cover, every selected object is constant with value its fibre at the selected point. Initial members may be discarded. This proves the last assertion. \end{proof} \begin{corollary}[The visible pro-homotopy type] \label{pf:cor-visible} Let $P\in\operatorname{Pro}(\Sps_\pi)$ have no prescribed uniform truncation bound, and define $\mathcal C_n(P)$ by \eqref{pf:eq-continuous-families}. Put $P^{(n+1)}=\{\tau_{\leq n+1}P_i\}_i$. Then \[ \mathcal C_n(P)\simeq\mathcal C_n(P^{(n+1)}), \qquad \Mod_n(\mathcal C_n(P)) \simeq\operatorname{mat}(P^{(n+1)}). \] The uniform finite parameter condition holds precisely when $P^{(n+1)}$ is a constant $\pi$-finite prospace. \end{corollary} \begin{proof} Apply Lemma~\ref{lem:base-truncation} at each finite stage and then Theorems~\ref{pf:thm-duality} and~\ref{pf:thm-uniform}. \end{proof} \begin{example}[Objectwise elimination without a uniform atlas] \label{pf:ex-zp} Let $P=\{B(\mathbb Z/p^r)\}_{r\geq1}$. For $n=0$, $\mathcal C_0(P)$ is the category of finite continuous $\mathbb Z_p$-sets. Every finite family of such sets is trivialized by the finite cover $\mathbb Z_p/p^r\mathbb Z_p$ for sufficiently large $r$. No finite local-section atlas exists. Indeed, a proposed finite atlas is a finite collection of finite continuous $\mathbb Z_p$-sets. There is an $r$ such that $p^r\mathbb Z_p$ fixes every point of all these sets. Put $A=\mathbb Z_p/p^{r+1}\mathbb Z_p$. For any nonempty member $U$ of the proposed atlas, the object $A\times U\to U$ has no section: the stabilizer of each point of $U$ contains $p^r\mathbb Z_p$, and this subgroup has no fixed point in $A$. This noninitial slice object consequently cannot be covered by copies of the slice terminal object. For every $n\geq0$, the same absence of a uniform atlas also follows from Theorem~\ref{pf:thm-uniform}, since \[ \Mod_n(\mathcal C_n(P)) \simeq B(\mathbb Z_p^{\mathrm{disc}}) \] has an infinite fundamental group. Here the quotient homomorphisms are surjective, so their inverse system has trivial $\lim^1$ and the homotopy limit is the classifying space of the abstract inverse limit group. Thus finite elimination for each prescribed family does not supply a common system of parameters for all finite semantics. The same example marks a boundary for the universal-parameter theorem. The forgetful exact functor $\omega:\mathcal C_0(P)\to\operatorname{FinSet}$ has no left adjoint in finite continuous sets. Such an adjoint would give a finite object $Q=\omega_!(1)$ representing $A\mapsto\omega(A)$. The object $Q$ must be nonempty, by testing $A=\varnothing$. Choose $r$ such that $p^r\mathbb Z_p$ fixes every point of $Q$. Then $\operatorname{Hom}_{\mathbb Z_p} (Q,\mathbb Z_p/p^{r+1}\mathbb Z_p)$ is empty, although the underlying target set is nonempty, a contradiction. \end{example} \begin{example}[The ordinary model space does not retain continuity] \label{pf:ex-cantor} Let $K=\{0,1\}^{\mathbb N}$ be the Cantor profinite set and let $K'=K\amalg\{*\}$. For every $n\geq0$, the model spaces of $\mathcal C_n(K)$ and $\mathcal C_n(K')$ are the underlying discrete sets $K$ and $K'$, respectively. These sets have the same cardinality, so the model spaces are equivalent as unstructured spaces. The semantic categories are not equivalent. Their posets of subterminal objects are the Boolean algebras of clopen subsets of $K$ and $K'$. The first is atomless: every nonempty clopen subset of the Cantor set contains two disjoint nonempty clopen subsets. The second has the atom $\{*\}$. An equivalence of categories preserves terminal objects, monomorphisms, and their subobject posets, so it cannot identify these two categories. Theorem~\ref{pf:thm-duality} retains continuity through the pro-object. The conservativity assertion in that theorem applies to a specified pro-morphism; it does not identify an arbitrary equivalence of underlying model spaces with a continuous morphism. \end{example} \section{Higher families and truncation} \label{hx:section-em} For a $\pi$-finite space $X$, put \[ \mathcal C_X=(\mathcal S_\pi)_{/X},\qquad \mathcal L_m(X)=\operatorname{Fun} (X,\mathcal S_{\pi,\leq m}),\qquad m\geq0. \] The second category is identified with the full subcategory of $\mathcal C_X$ consisting of maps whose homotopy fibres are $m$-truncated. The truncation is relative to $X$. \begin{lemma}\label{hx:finite-fibres} If $X$ is $\pi$-finite, a map $E\to X$ has $\pi$-finite homotopy fibres if and only if $E$ is $\pi$-finite. Consequently \[ \mathcal C_X\simeq\operatorname{Fun}(X,\mathcal S_\pi). \] \end{lemma} \begin{proof} For a homotopy fibre $F$ over a point of $X$, the long exact homotopy sequence shows that finite homotopy groups and a truncation bound for $E$ and $X$ imply the same properties for $F$. Its components are finite as well: they lie over the finitely many components of $E$, and the possible components over any one of them form a quotient of the finite group $\pi_1(X)$. Conversely, choose one point in every component of $X$. There are only finitely many chosen fibres. Their homotopy groups are finite and their truncation bounds have a finite maximum. The homotopy sequence gives these properties for $E$, whose components form a quotient of the disjoint union of the component sets of the chosen fibres. The displayed equivalence is the usual classification of families of spaces over an $\infty$-groupoid by functors from it. \end{proof} The category $\mathcal C_X$ is the bounded coherent part of $\mathcal S_{/X}$. Fixed relative truncation bounds give the categories $\mathcal L_m(X)$ used below. Quotients in the full bounded coherent category can increase a truncation bound, so these two categories have different closure properties. \begin{theorem}[Sharpness of the family truncation bound] \label{hx:sharp-family-bound} Let $A$ be a nonzero finite abelian group, let $r\geq1$, and set $X=K(A,r+1)$, with its standard base point $x$. Then the following statements hold. \begin{enumerate} \item For $0\leq m\leq r-1$, evaluation at $x$ induces an equivalence \[ \mathcal L_m(X)\xrightarrow{\sim}\mathcal S_{\pi,\leq m}. \] An inverse sends a space to its constant family. \item The point object $P_x=(*\xrightarrow{x}X)$ belongs to $\mathcal L_r(X)$ and is not a constant family. \item Its endomorphism space in the slice is \[ \operatorname{Map}_{\mathcal C_X}(P_x,P_x) \simeq\Omega_xX\simeq K(A,r). \] Every endomorphism in this space is an equivalence. \end{enumerate} \end{theorem} \begin{proof} An object $F$ of $\mathcal S_{\pi,\leq m}$ has an $m$-truncated self-equivalence space. The component of $F$ in the core $(\mathcal S_{\pi,\leq m})^\simeq$ is therefore the $(m+1)$-type $B\operatorname{Aut}(F)$. Since $X$ is connected, every functor from $X$ lands in one such component. Since $X$ is $r$-connected and $m+1\leq r$, evaluation induces an equivalence \[ \operatorname{Map}(X,B\operatorname{Aut}(F)) \simeq B\operatorname{Aut}(F). \] Thus every object of $\mathcal L_m(X)$ is a constant family. For constant families $F,G$, their mapping space is \[ \operatorname{Map}_{\mathcal L_m(X)}(F_X,G_X) \simeq\operatorname{Map} \bigl(X,\operatorname{Map}(F,G)\bigr). \] The inner mapping space is $m$-truncated, so evaluation is again an equivalence. This proves the first statement. The homotopy fibre of $P_x$ is $\Omega X\simeq K(A,r)$, which is $\pi$-finite and $r$-truncated. A constant family with that fibre has a section. A section of $P_x$ would contract $X$, which is impossible because $A\ne0$. Finally, the slice mapping-space formula identifies $\operatorname{Map}_{/X}(P_x,P_x)$ with the homotopy fibre of the base-point map $*\to X$, namely $\Omega X$. All these maps have an equivalence as their underlying map of total spaces, so they are equivalences in the slice. \end{proof} In particular, for every finite abelian $A$, \[ \mathcal L_0(K(A,2))\simeq\mathbf{FinSet}. \] The ordinary fundamental groupoid of $K(A,2)$ is terminal. The first relative truncation level already contains the point object, with self-equivalence space $BA$. Thus both finite-set semantics and the ordinary fundamental groupoid lose information that is present in the next family level. More generally, Theorem~\ref{hx:sharp-family-bound} shows that $r$-truncated families can require the $(r+1)$-type of the base. \begin{corollary}\label{hx:ordinary-models} For every finite abelian $A$, the zero-truncated part of $\mathcal C_{K(A,2)}$ is $\mathbf{FinSet}$, and its groupoid of set-valued models preserving finite limits, finite coproducts, and effective epimorphisms, with natural isomorphisms as arrows, is terminal. These data are independent of $A$, while the point object's higher self-equivalence space is $BA$. \end{corollary} \begin{proof} The category assertion is Theorem~\ref{hx:sharp-family-bound}. A functor $\mathbf{FinSet}\to\mathbf{Set}$ with these preservation properties sends the terminal object to a singleton and sends every finite set, expressed as a finite coproduct of singletons, to that same finite set up to a unique compatible isomorphism. These isomorphisms commute with every function. Every natural automorphism is the identity, since it is the identity on the terminal object and commutes with all point maps. \end{proof} \subsection{A computable family of higher torsors} For a finite abelian group $B$, the space $K(B,r)$ is a group object whose delooping is $K(B,r+1)$. A principal $K(B,r)$-bundle over $X$ is classified by a map $X\to K(B,r+1)$. The group object and its action are retained in this classification. For $r=1$ these are gerbes with fixed constant abelian band $B$. \begin{proposition}\label{hx:em-torsors} Let $A,B$ be finite abelian groups and let $r\geq1$. The moduli space of principal $K(B,r)$-bundles over $K(A,r+1)$ is \[ \operatorname{Map}(K(A,r+1),K(B,r+1)) \simeq\operatorname{Hom}(A,B)\times K(B,r+1). \] In particular, its equivalence classes are naturally indexed by homomorphisms $\alpha:A\to B$. The family corresponding to $\alpha$ can be represented by \[ E_\alpha=\operatorname{hofib}\bigl(K(\alpha,r+1)\bigr) \longrightarrow K(A,r+1). \] Its total space is connected and $\pi$-finite, with \[ \pi_{r+1}(E_\alpha)\cong\ker\alpha, \qquad \pi_r(E_\alpha)\cong\operatorname{coker}\alpha, \] and with all other positive-degree homotopy groups zero. The family has a section exactly when $\alpha=0$. \end{proposition} \begin{proof} Eilenberg--Mac Lane representability and the Hurewicz theorem give \[ [K(A,r+1),K(B,r+1)]_* =H^{r+1}(K(A,r+1);B) \cong\operatorname{Hom}(A,B). \] The universal coefficient exact sequence has no Ext term in this degree, since $H_r(K(A,r+1);\mathbb Z)=0$. The positive homotopy groups of the pointed mapping space are the reduced cohomology groups in degrees below $r+1$, all of which vanish by $r$-connectedness. Hence this pointed mapping space is the discrete space $\operatorname{Hom}(A,B)$. The abelian group structure on $K(B,r+1)$ splits evaluation at the base point: subtracting the value at that point identifies the unpointed mapping space with the product of the pointed mapping space and $K(B,r+1)$. Pulling back the path fibration of $K(B,r+1)$ along $K(\alpha,r+1)$ gives the displayed family. Its homotopy sequence reduces in positive degrees to \[ 0\longrightarrow\pi_{r+1}(E_\alpha) \longrightarrow A\xrightarrow{\alpha}B \longrightarrow\pi_r(E_\alpha)\longrightarrow0. \] Its fibre is the connected space $K(B,r)$, so its total space is connected. The sequence proves $\pi$-finiteness and the homotopy-group assertions. A section is a nullhomotopy of the classifying map. By the first calculation this exists precisely when $\alpha=0$. \end{proof} For $A=B$ and $\alpha=\mathrm{id}$, the total space $E_\alpha$ is contractible and the family is the point object of Theorem~\ref{hx:sharp-family-bound}. For $\alpha=0$ it is the product $K(A,r+1)\times K(B,r)$. Already $A=B=C_2$ and $r=1$ give two inequivalent finite-band families over a base whose finite-set semantics is $\mathbf{FinSet}$. As $B$ varies, the pointed classes give the functor $B\mapsto\operatorname{Hom}(A,B)$ on finite abelian groups, which determines $A$ by Yoneda. \subsection{An explicit finite simplicial presentation} For a finite abelian group $A$, use the standard simplicial abelian group whose $q$-simplices are normalized $2$-cocycles on $\Delta^q$ with coefficients in $A$. Such a simplex is a collection \[ (a_{ijk})_{0\leq i