% Standalone submission source. Compile with latexmk -pdf main.tex. % The bibliography is embedded; no external source or figure files are needed. \documentclass[11pt,a4paper]{article} \usepackage[margin=28mm]{geometry} \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} \usepackage{microtype} \usepackage{mathtools,amssymb,amsthm} \usepackage{newpxtext,newpxmath} \usepackage{mathrsfs} \usepackage{tikz-cd,enumitem} \usepackage{xcolor} \definecolor{paperlink}{RGB}{0,0,114} \usepackage{hyperref} \urlstyle{same} \hypersetup{colorlinks=true,linktoc=all,linkcolor=paperlink,citecolor=paperlink,urlcolor=paperlink,pdftitle={Isomorphism Loci and Coherence in Equivalence Extension},pdfauthor={Zhenyu Sun},pdfstartview=Fit} \usepackage{titling,titlesec} \setlength{\droptitle}{-2.5em} \pretitle{\begin{center}\LARGE} \posttitle{\par\end{center}\vspace{0.3em}} \preauthor{\begin{center}\normalsize} \postauthor{\par\end{center}} \predate{}\postdate{} \titleformat{\section}{\large\bfseries}{\thesection}{0.65em}{} \titleformat{\subsection}{\normalsize\bfseries}{\thesubsection}{0.65em}{} \titlespacing*{\section}{0pt}{2.1ex plus .6ex minus .2ex}{1ex plus .2ex} \titlespacing*{\subsection}{0pt}{1.7ex plus .4ex minus .2ex}{.7ex plus .2ex} \pagestyle{plain} \setlength{\parindent}{1.25em} \setlength{\parskip}{0pt} \setlength{\emergencystretch}{1em} \setcounter{tocdepth}{1} \numberwithin{equation}{section} \newtheorem{theorem}{Theorem}[section] \newtheorem{lemma}[theorem]{Lemma} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \newtheorem{hypothesis}[theorem]{Hypothesis} \newtheorem{construction}[theorem]{Construction} \newtheorem{example}[theorem]{Example} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \newcommand{\E}{\mathcal E} \newcommand{\D}{\mathcal D} \newcommand{\Cof}{\mathsf{Cof}} \newcommand{\TC}{\mathsf{TCof}} \newcommand{\Fib}{\mathsf{Fib}} \newcommand{\TF}{\mathsf{TFib}} \newcommand{\W}{\mathcal W} \newcommand{\id}{\mathrm{id}} \DeclareMathOperator{\Hom}{Hom} \DeclareMathOperator{\Ext}{Ext} \DeclareMathOperator{\IsoLoc}{Iso} \DeclareMathOperator{\Loc}{Loc} \DeclareMathOperator{\Comp}{Comp} \DeclareMathOperator{\Sub}{Sub} \DeclareMathOperator{\im}{im} \DeclareMathOperator{\Aut}{Aut} \newcommand{\graph}[1]{\langle #1\rangle} \newcommand{\sSet}{\mathbf{sSet}} \newcommand{\Set}{\mathbf{Set}} \newcommand{\simeqto}{\xrightarrow{\sim}} \newcommand{\xto}[1]{\xrightarrow{#1}} \setlist[enumerate]{label=\textup{(\roman*)},leftmargin=2.6em} \setlist[itemize]{leftmargin=1.8em} \title{Isomorphism Loci and Coherence\\in Equivalence Extension} \author{Zhenyu Sun} \date{} \begin{document} \maketitle \begin{abstract} We study the restriction data carried by dependent-product extension along a monomorphism. In a locally cartesian closed category, the extended map is an isomorphism after a change of base if and only if the input map is an isomorphism on the restricted base. In a topos, its isomorphism locus is therefore the universal quantification of the input locus. A terminal characterization gives coherent comparisons for base change and successive extension, together with formulas for intersections and unions. Under explicit homotopical, cartesian, and universe hypotheses, this construction gives equivalence extension and preserves the boundary identifications used to prove fibrancy of a universe. Graph comparisons and strict fillers of a fixed universe boundary are represented by trivially fibrant objects. A single realignment over the comparison object induces a weak equivalence between these parameter objects, and both admit extensions of every finite cubical boundary. A finite-groupoid example shows that graph comparisons cannot be selected naturally under all isomorphisms of unstructured input. \end{abstract} \begin{center} \begin{minipage}{0.9\textwidth} \small \emph{2020 Mathematics Subject Classification.} 18N40, 18B25, 03G30, 55U35.\par \emph{Keywords.} Equivalence extension, dependent product, isomorphism locus, Beck--Chevalley, realignment, fibrant universe. \end{minipage} \end{center} {\small\tableofcontents} \clearpage \section{Introduction} Let $k:X'\hookrightarrow X$ be a monomorphism, let $q:B\to X$ be a family, and write $B'=X'\times_X B$. A map $e:A'\to B'$ can be extended to a map with codomain $B$ by taking the dependent product along the induced monomorphism $b:B'\hookrightarrow B$: \begin{equation}\label{intro:extension} w=\Pi_b(e):A\longrightarrow B. \end{equation} The restriction $b^*w$ is canonically isomorphic to $e$. Under suitable homotopical assumptions, if $A'\to X'$ and $B\to X$ are fibrations and $e$ is a relative equivalence, then $A\to X$ is a fibration and $w$ is a relative equivalence. This is the dependent-product construction underlying the equivalence extension property. The construction is especially useful when a second restriction has to be preserved. In the proof of fibrancy of a cubical universe, the first restriction is a boundary cylinder and the second is a graph. Their intersection carries a specified isomorphism. A weak equivalence on the second restriction would not solve the classification problem: the specified family must be recovered there by an actual isomorphism. The interaction of these two restrictions is the starting point of this paper. The restriction criterion is exact. For an arbitrary map $s:T\to X$, let $s':T\times_X X'\to X'$ be its pullback. Then Theorem~\ref{rel:exact} gives \begin{equation}\label{intro:exact} s^*\Ext_k(e)\text{ is an isomorphism} \quad\Longleftrightarrow\quad (s')^*e\text{ is an isomorphism}. \end{equation} Here $\Ext_k(e)$ denotes \eqref{intro:extension}, regarded as a map over $X$ with fixed codomain $B$. The counit of $b^*\dashv\Pi_b$ identifies the restricted map with the input. Remark~\ref{rel:specified-target} explains how the same counit retains a compatible identification with another specified representative of the target family. In an elementary topos, the parameters on which a map is an isomorphism form a subobject, and \eqref{intro:exact} becomes \begin{equation}\label{intro:locus} \IsoLoc_X(\Ext_k(e))=\forall_k\IsoLoc_{X'}(e). \end{equation} Viewing $X'$ and the original locus $R$ as subobjects of $X$, the right side is the Heyting implication $X'\Rightarrow R$ (Theorem~\ref{rel:locus-formula}). Thus the construction determines all isomorphism restrictions at once, including compatible identifications inherited from $e$. Coherence follows from a terminal characterization. The dependent-product extension is terminal among objects equipped with an identification of their restriction with $e$. Among these objects it is characterized, up to a unique identification-preserving isomorphism, by invertibility of the unit to $\Pi_b b^*$. This determines the comparisons for base change and successive extension, including their unit, associativity, and mixed laws (Section~\ref{coh:section}). For subobjects $V,W\hookrightarrow B$ in a topos, the corresponding locality functors satisfy \[ \Loc_V\Loc_W\cong\Loc_{V\cap W}\cong\Loc_W\Loc_V, \qquad \Loc_{V\cup W}P\cong \Loc_VP\times_{\Loc_{V\cap W}P}\Loc_WP. \] Section~\ref{cat:lattice-section} proves these formulas and the corresponding gluing formula for different families on overlapping domains. The homotopical application begins with a choice of comparison. Under the assumptions of Section~\ref{hom:section}, two fibrations over a common base that receive trivial cofibrations from a common object admit a comparison, and every such comparison is a relative homotopy equivalence. With the cartesian assumptions of Section~\ref{cmp:section}, these comparisons are represented by an object $Q$ with $Q\to1$ a trivial fibration. Applying \eqref{intro:extension} to the universal comparison and then realigning once over $Q$ produces a family of strict universe fillers compatible with specialization. The object $H_\chi$ of all strict fillers of the fixed boundary classifier $\chi$ is also trivially fibrant, and the constructed family induces a weak equivalence $Q\to H_\chi$ (Theorems~\ref{uni:parameter} and \ref{uni:all-fillers}). Every finite cubical boundary of strict fillers therefore extends, including those arising from different comparison and realignment choices. These are statements about maps into the universe with fixed boundary value. Trivial fibrancy of the parameter objects does not provide a natural point. In Proposition~\ref{ex:graph-choice}, an automorphism of finite-groupoid graph data has no fixed comparison. This rules out a selector natural under all isomorphisms of the unstructured data, while leaving the coherence of the specified dependent-product extension intact. \subsection*{Relation to previous work} The equivalence extension property is closely related to the gluing constructions of cubical type theory \cite[\S6]{CCHM2018}. Shulman's condition $(4')$ gives an earlier equivalence-extension formulation in presheaf models \cite{Shulman2015}. Sattler gave a general categorical treatment and used it to construct model structures \cite{Sattler2017}. Awodey's proof of fibrancy of the universe uses graph comparison, dependent-product extension, Beck--Chevalley, and realignment \cite[Propositions 116 and 120]{Awodey2023}; the monograph \cite{Awodey2026} provides the published account. The homotopical extension argument is also available in the general framework of cylindrical premodel categories \cite[Theorem 3.3.3]{ACCRS2026}. We include its proof in terms of a local unit square to specify the hypotheses used here. Dependent products, their canonical base-change comparisons, and localization at a subterminal object are standard categorical constructions; see \cite{Johnstone2002}. Our treatment organizes them around prescribed relative identifications, the exact locus formula \eqref{intro:locus}, and the distinction between coherent extension and comparison selection. Fibrancy of the universe is an application of these results. Realignment is used in its cartesian-square form, as in Shulman's condition $(2')$ \cite{Shulman2015}; universes of small maps satisfying realignment in Grothendieck topoi are constructed in \cite[Corollary~4.3.3]{GSS2026}. Strict substitution for structured type-theoretic operations is addressed by the local-universes construction \cite{LumsdaineWarren2015}; the symmetry obstruction in the present paper concerns unstructured input diagrams and does not contradict such coherence results. \subsection*{Conventions} Composition is written from right to left. A family over $X$ is an object of the slice $\E/X$. For $f:Y\to X$, the functors $f^*$ and $\Pi_f$ denote pullback and its right adjoint. Pullbacks and right adjoints are chosen once. Equalities involving their composites are interpreted through the specified canonical comparison isomorphisms unless strict equality is explicitly asserted. A specified identification is always part of the data. We use the word small only for an explicitly stated pullback-stable class of families or for a specified cardinal bound. \section{Dependent products and normalized extensions}\label{cat:section} Let $\E$ be a locally cartesian closed category. We choose pullbacks and right adjoints to the pullback functors, and retain the canonical comparison isomorphisms between successive pullbacks. For a map $b:B'\to B$, write \[ b^*:\E/B\longrightarrow\E/B',\qquad \Pi_b:\E/B'\longrightarrow\E/B, \qquad b^*\dashv\Pi_b. \] An object $e:E'\to B'$ of a slice is identified with its structure map when it occurs as an argument of $\Pi_b$. The terminal object of $\E/B$ is $\id_B:B\to B$. Accordingly, an object of this slice is terminal precisely when its structure map is an isomorphism. All the constructions in this section concern the underlying categories of families. \begin{lemma}[Restriction of a dependent product]\label{cat:counit} If $b:B'\hookrightarrow B$ is a monomorphism, the counit \[ \varepsilon_e:b^*\Pi_b(e)\longrightarrow e \] is an isomorphism for every $e\in\E/B'$. Consequently $\Pi_b$ is fully faithful and preserves terminal objects. \end{lemma} \begin{proof} Let $\Sigma_b:\E/B'\to\E/B$ denote composition with $b$. Since $b$ is monic, the canonical map $b^*\Sigma_b(T)\to T$ is an isomorphism. For any $T\in\E/B'$, the two adjunctions give natural bijections \begin{align*} \Hom_{B'}(T,b^*\Pi_b e) &\cong\Hom_B(\Sigma_bT,\Pi_be)\\ &\cong\Hom_{B'}(b^*\Sigma_bT,e) \cong\Hom_{B'}(T,e). \end{align*} These bijections are induced by composition with the counit. Yoneda's lemma proves that $\varepsilon_e$ is invertible. The full faithfulness is the standard counit criterion, and terminal-object preservation follows because $\Pi_b$ is a right adjoint. \end{proof} For a fixed monomorphism $b:B'\hookrightarrow B$, put \[ \Loc_b=\Pi_b b^*:\E/B\longrightarrow\E/B, \qquad \eta^b:\id\longrightarrow\Loc_b. \] Call $F\in\E/B$ \emph{$b$-local} when $\eta^b_F$ is an isomorphism. This is the usual locality associated with restriction to a subobject; it records exactly which families are determined by dependent-product extension of their restrictions. \begin{proposition}[Locality and uniqueness]\label{cat:locality} The following statements hold. \begin{enumerate} \item An object is $b$-local if and only if it is isomorphic to $\Pi_b(e)$ for some $e\in\E/B'$. \item The functor $\Loc_b$ is left exact and idempotent. It is a reflector onto the full subcategory of $b$-local objects. \item If $F,G$ are $b$-local, restriction induces a bijection \[ \Hom_B(F,G)\xrightarrow{\cong} \Hom_{B'}(b^*F,b^*G). \] \item Given a $b$-local object $F$ and an isomorphism $\rho:b^*F\xrightarrow{\cong}e$, there is a unique isomorphism $\bar\rho:F\xrightarrow{\cong}\Pi_b(e)$ such that $\varepsilon_e b^*\bar\rho=\rho$. \end{enumerate} \end{proposition} \begin{proof} The triangle identity and Lemma~\ref{cat:counit} imply that $\eta^b_{\Pi_be}$ is invertible. Conversely, if $\eta^b_F$ is invertible, it exhibits $F$ as $\Pi_b(b^*F)$. Both $b^*$ and $\Pi_b$ preserve finite limits, and the multiplication \[ \Pi_bb^*\Pi_bb^*\xrightarrow{\Pi_b\varepsilon b^*}\Pi_bb^* \] is an isomorphism. The adjunction identifies maps from $F$ to a local object $\Pi_b(e)$ with maps from $b^*F$ to $e$; this proves the reflector assertion. For local $G$, the same adjunction identifies $\Hom_B(F,G)$ with $\Hom_{B'}(b^*F,b^*G)$, proving the third assertion. Finally, the required map is \[ \bar\rho=\Pi_b(\rho)\,\eta^b_F. \] It is invertible, and the counit and triangle identities give its stated restriction. The third assertion proves uniqueness. \end{proof} \begin{definition}[Normalized relative extension]\label{cat:extension} Let $k:X'\hookrightarrow X$ be a monomorphism and $q:B\to X$ a map. Form \[ B'=X'\times_XB,\qquad b:B'\hookrightarrow B, \qquad q':B'\to X'. \] For an object $e:E'\to B'$ define its \emph{normalized relative extension} by \[ \Ext_{k,q}(e)=\Pi_b(e)= (w:E\longrightarrow B). \] The associated family over $X$ is $p=qw:E\to X$. Its specified restriction is the counit isomorphism $b^*w\cong e$. \end{definition} \begin{corollary}[Characterization of the extension]\label{cat:characterization}\label{cat:rigidity} The pair consisting of $\Ext_{k,q}(e)$ and its counit restriction is the unique $b$-local extension of $e$, up to a unique isomorphism preserving the restriction. Moreover, for $e,d\in\E/B'$ there is a natural bijection \[ \Hom_B(\Ext_{k,q}(e),\Ext_{k,q}(d)) \cong\Hom_{B'}(e,d). \] Thus maps, isomorphisms, and automorphisms of the input extend uniquely between the normalized extensions. \end{corollary} \begin{proof} Apply Proposition~\ref{cat:locality} to $b$ and use the two counit isomorphisms. Invertibility is preserved by $\Pi_b$ and reflected by restriction, so the assertion also applies to isomorphisms and automorphisms. \end{proof} \begin{proposition}[Terminal extension]\label{cat:terminal-extension} Fix $e\in\E/B'$. Let $\mathcal{X}_b(e)$ have as objects the pairs $(F,\rho)$ with $F\in\E/B$ and $\rho:b^*F\xrightarrow{\cong}e$, and as morphisms $(F,\rho)\to(G,\sigma)$ the maps $t:F\to G$ over $B$ satisfying $\sigma b^*t=\rho$. Then $(\Pi_be,\varepsilon_e)$ is a terminal object of $\mathcal{X}_b(e)$. Its unique receiving map from $(F,\rho)$ is an isomorphism precisely when $F$ is $b$-local. \end{proposition} \begin{proof} Adjunction identifies maps $t:F\to\Pi_be$ with maps $b^*F\to e$ by $t\mapsto\varepsilon_e b^*t$. Thus there is exactly one such $t$ with transpose $\rho$, namely $\Pi_b(\rho)\eta^b_F$. Since $\rho$ is invertible, this map is invertible if and only if $\eta^b_F$ is. This is the defining locality condition. \end{proof} \begin{remark}\label{cat:normalization} For $k=\id_X$, the extension is canonically the input. If $e$ is an isomorphism, the extension is canonically $\id_B$, with the counit identifying its restriction with the specified isomorphism $e$. The normalization concerns the actual arrow to the fixed target $B$. Isomorphisms to the terminal object of a slice are unique; external boundary markings may still involve nontrivial automorphisms, as in Remark~\ref{rel:specified-target}. \end{remark} \section{Isomorphism restrictions and their loci}\label{rel:section} Retain the data of Definition~\ref{cat:extension}. For any map $s:T\to X$, write \[ T'=T\times_XX',\quad k_T:T'\hookrightarrow T,\quad B_T=T\times_XB,\quad B'_{T'}=T'\times_{X'}B'. \] Let $e_{T'}$ and $w_T$ denote the corresponding pullbacks of $e$ and $w=\Ext_{k,q}(e)$. \begin{lemma}[Beck--Chevalley]\label{rel:bc} There is a canonical isomorphism \[ \theta_s:w_T\xrightarrow{\cong} \Ext_{k_T,q_T}(e_{T'}) \] in $\E/B_T$. After restriction to $B'_{T'}$, this isomorphism identifies the counit restrictions on both sides. \end{lemma} \begin{proof} Consider the pullback square of total spaces \[ \begin{tikzcd} B'_{T'}\arrow[r,"s'_{B}"]\arrow[d,hook,"b_T"']& B'\arrow[d,hook,"b"]\\ B_T\arrow[r,"s_B"']&B. \end{tikzcd} \] For $H\in\E/B_T$, the adjunctions and the pullback square give \begin{align*} \Hom_{B_T}(H,s_B^*\Pi_be) &\cong\Hom_B(\Sigma_{s_B}H,\Pi_be)\\ &\cong\Hom_{B'}(b^*\Sigma_{s_B}H,e)\\ &\cong\Hom_{B'}(\Sigma_{s'_B}b_T^*H,e)\\ &\cong\Hom_{B'_{T'}}(b_T^*H,(s'_B)^*e)\\ &\cong\Hom_{B_T}(H,\Pi_{b_T}(s'_B)^*e). \end{align*} The middle isomorphism follows directly by computing the indicated pullback. Yoneda's lemma gives $\theta_s$. Tracing the identity map through these adjunctions shows that its restriction, followed by the target counit, is the pullback of the source counit. This is the asserted compatibility. \end{proof} \begin{theorem}[Exact preservation of isomorphism restrictions] \label{rel:exact} For every map $s:T\to X$, \[ w_T\text{ is an isomorphism} \quad\Longleftrightarrow\quad e_{T'}\text{ is an isomorphism}. \] If the input restriction is a prescribed isomorphism $\alpha:e_{T'}\xrightarrow{\cong}\id_{B'_{T'}}$ in the slice, then $w_T$ has a canonical identification with $\id_{B_T}$ whose restriction is $\alpha$, after the counit comparison. These identifications are compatible with every further pullback. In particular the construction simultaneously preserves any collection of prescribed isomorphism restrictions inherited from the input arrow $e$. \end{theorem} \begin{proof} By Lemma~\ref{rel:bc}, $w_T$ is canonically $\Pi_{b_T}(e_{T'})$. If $e_{T'}$ is terminal in its slice, its dependent product is terminal, so $w_T$ is an isomorphism. Conversely, if $w_T$ is terminal, then its restriction along $b_T$ is terminal. The counit identifies that restriction with $e_{T'}$. For the specified identification, apply $\Pi_{b_T}$ to $\alpha$ and compose with the canonical terminal-object comparison and $\theta_s$. The counit naturality square shows that its restriction is $\alpha$. Further pullback gives another arrow from the same object to the terminal object in the resulting slice. Such an arrow is unique. Hence the two ways of obtaining the identification agree, with the canonical pullback comparisons understood. This also proves compatibility on intersections of any prescribed restrictions. \end{proof} \begin{remark}\label{rel:specified-target} The map to the terminal object in Theorem~\ref{rel:exact}, when invertible, is the unique such identification in the slice. Independent marking data enter when the restricted family is identified with an externally specified family, as follows. Suppose a restriction is to be identified with a family $P\to T$ and an isomorphism $\lambda:P\xrightarrow{\cong}B_T$ is specified. Write $E'_{T'}$ for the domain of $e_{T'}$, and suppose an isomorphism $\rho:E'_{T'}\xrightarrow{\cong}P|_{T'}$ is given with $e_{T'}=\lambda|_{T'}\rho$. Then the resulting identification is $\lambda^{-1}w_T$, and its restriction is exactly $\rho$ under the counit. Thus the theorem also retains a specified representative of the restricted target family. For several such markings the construction respects every compatibility relation inherited from the input, since all the markings are obtained from the same restricted arrow $w_T$. \end{remark} For the remainder of this section assume that $\E$ is a topos. Its internal logic provides an exact description of the loci in Theorem~\ref{rel:exact}. For a family $q:B\to X$ and an arrow $v:E\to B$ over $X$, let $\IsoLoc_X(v)$ denote the subobject of $X$ defined by \[ x\in\IsoLoc_X(v) \quad\Longleftrightarrow\quad \forall b\in B_x\;\exists!a\in E_x\;(v(a)=b). \] This definition involves unique existence in the internal logic, and therefore applies to generalized elements as well as global points. \begin{lemma}[Representability and stability of the isomorphism locus] \label{rel:locus-exists} The subobject $\IsoLoc_X(v)\hookrightarrow X$ exists and satisfies \[ s:T\to X\text{ factors through }\IsoLoc_X(v) \quad\Longleftrightarrow\quad s^*v\text{ is an isomorphism}. \] It is stable under arbitrary base change. In particular it is the largest subobject of $X$ on which $v$ is an isomorphism. \end{lemma} \begin{proof} We first work over $B$. Write $J=\operatorname{im}(v)\hookrightarrow B$, let $r:E\times_BE\to B$ be the structure map, and regard the diagonal $\Delta_v:E\hookrightarrow E\times_BE$ as a subobject. The subobject \[ J\cap\forall_r(\Delta_v)\hookrightarrow B \] asserts that a fibre is inhabited and has at most one element. Here $\forall_r$ is the right adjoint to inverse image on subobject lattices; it exists in a topos. On a pullback of this locus, $v$ is both epimorphic and monomorphic, hence an isomorphism. Conversely, any pullback on which $v$ is an isomorphism satisfies these two conditions. This constructs $\IsoLoc_B(v)$. Now set \[ \IsoLoc_X(v)=\forall_q\bigl(\IsoLoc_B(v)\bigr). \] The adjunction for $\forall_q$ says precisely that a test object over $X$ factors through this subobject when its pullback of $v$ is an isomorphism. More explicitly, images are stable under pullback, diagonal subobjects pull back to diagonal subobjects, and the right adjoints on subobjects satisfy Beck--Chevalley. Therefore each displayed construction commutes with substitution along an arbitrary $s:T\to X$. On $T$, the condition that the resulting subobject is all of $T$ is equivalent to $s^*v$ being an isomorphism. This proves the claimed factorization criterion and stability. Applying the criterion to subobject inclusions proves maximality. \end{proof} \begin{theorem}[Exact locus formula]\label{rel:locus-formula}\label{rel:locus} Let $R'=\IsoLoc_{X'}(e)\hookrightarrow X'$, where $e$ is viewed as an arrow between the families $E'\to X'$ and $B'\to X'$. Then \[ \IsoLoc_X\bigl(\Ext_{k,q}(e)\bigr)=\forall_k(R'). \] If $R\hookrightarrow X$ denotes the composite $R'\hookrightarrow X'\hookrightarrow X$, this can equivalently be written in the Heyting algebra $\operatorname{Sub}(X)$ as \[ \IsoLoc_X\bigl(\Ext_{k,q}(e)\bigr)=(X'\Rightarrow R). \] \end{theorem} \begin{proof} For a subobject $T\hookrightarrow X$, Lemma~\ref{rel:locus-exists} and Theorem~\ref{rel:exact} give successive equivalences \begin{align*} T\leq\IsoLoc_X(w) &\Longleftrightarrow w_T\text{ is an isomorphism}\\ &\Longleftrightarrow e_{T\times_XX'}\text{ is an isomorphism}\\ &\Longleftrightarrow k^*T\leq R'\\ &\Longleftrightarrow T\leq\forall_k(R'). \end{align*} Thus the two subobjects are equal. Under the inclusion of $\operatorname{Sub}(X')$ into $\operatorname{Sub}(X)$, the condition $k^*T\leq R'$ is $T\cap X'\leq R$. The defining adjunction for Heyting implication identifies its largest solution with $X'\Rightarrow R$. \end{proof} \begin{example}[Boolean and non-Boolean boundaries]\label{rel:boolean} In a Boolean topos the formula becomes \[ \IsoLoc_X(w)=(X\setminus X')\cup R. \] In a general topos the Heyting implication is the appropriate operation. For example, in sheaves on $\mathbb R$, let $X=B=1$ and $q=\id_1$, let $X'$ be the subterminal corresponding to the open set $(0,1)$, and let $e$ be the empty family over $X'$. Then $R'=0$ and the extended family is an isomorphism precisely on the open set \[ (-\infty,0)\cup(1,\infty), \] which represents $\neg X'=\operatorname{int}(\mathbb R\setminus(0,1))$. This example concerns the categorical extension and its exact locus. \end{example} \section{Base change and successive extension} \label{coh:section} The comparison maps above satisfy coherence laws determined by their restrictions. This gives a direct way to verify all the relevant diagrams without imposing additional coherence choices on the dependent products. \begin{theorem}[Coherent change of base]\label{coh:basechange} For $s:T\to X$, the Beck--Chevalley isomorphisms \[ \theta_s:s^*\Ext_{k,q}(e) \xrightarrow{\cong}\Ext_{k_T,q_T}(e_{T'}) \] are natural in $e$. They satisfy the identity and composition laws: the comparison for $\id_X$ is the canonical identity comparison, and for $r:S\to T$ the comparison for $sr$ agrees with the composite obtained by pulling back $\theta_s$ along $r$ and then applying $\theta_r$. All these comparisons preserve the specified restrictions and the isomorphisms of Theorem~\ref{rel:exact}. \end{theorem} \begin{proof} The Hom-set construction in Lemma~\ref{rel:bc} is natural in $e$, so $\theta_s$ is natural. That lemma also identifies $s^*\Ext_{k,q}(e)$ as a $b_T$-local object, equipped with its counit identification on $B'_{T'}$. For the identity law, both the Beck--Chevalley map and the canonical identity comparison restrict to the identity on $e$. Proposition~\ref{cat:locality}(3) makes them equal. For composable $r,s$, transport both candidate maps along the canonical associativity comparisons for pullbacks. They are maps between the same two $b_S$-local objects in $\E/B_S$. Their restrictions are the same identity on the twice-reindexed input, by the counit compatibility in Lemma~\ref{rel:bc}. Restriction is faithful on local objects, so the maps are equal. The same argument applies to a morphism of inputs. Finally, the terminal-object identifications in Theorem~\ref{rel:exact} are unique in their respective slices, and hence are preserved by these comparisons. \end{proof} \begin{theorem}[Successive extension]\label{coh:successive}\label{coh:composition} Let \[ X_0\xrightarrow{k_1}X_1\xrightarrow{k_2}X_2 \] be monomorphisms, let $q_2:B_2\to X_2$, and put $B_i=X_i\times_{X_2}B_2$. Denote the induced monomorphisms by $b_1:B_0\hookrightarrow B_1$ and $b_2:B_1\hookrightarrow B_2$. For $e\in\E/B_0$ there is a canonical isomorphism \[ a_{b_2,b_1,e}:\Pi_{b_2}\Pi_{b_1}(e) \xrightarrow{\cong}\Pi_{b_2b_1}(e). \] It preserves the specified restriction to $B_0$, is natural in $e$, and has the following properties. \begin{enumerate} \item Extension along an identity is a two-sided unit. \item For three successive monomorphisms, the two composite associativity comparisons agree. \item Beck--Chevalley commutes with the successive-extension comparison under every change of the final base $X_2$. \end{enumerate} Consequently every parenthesization of a finite sequence of normalized extensions has a unique comparison with direct extension, and these comparisons commute with arbitrary substitution. \end{theorem} \begin{proof} For $H\in\E/B_2$, the adjunctions give \begin{align*} \Hom_{B_2}(H,\Pi_{b_2}\Pi_{b_1}e) &\cong\Hom_{B_1}(b_2^*H,\Pi_{b_1}e)\\ &\cong\Hom_{B_0}(b_1^*b_2^*H,e)\\ &\cong\Hom_{B_0}((b_2b_1)^*H,e). \end{align*} Thus $\Pi_{b_2}\Pi_{b_1}$ and $\Pi_{b_2b_1}$ are right adjoints to the same pullback functor. The resulting adjunction isomorphism is $a_{b_2,b_1,e}$. Its counit is the composite of the two counits, so it preserves the specified restriction and is natural in $e$. Both its source and target are $(b_2b_1)$-local. For an identity monomorphism, the canonical unit comparison and the displayed adjunction comparison have the same restriction, proving the unit law. For three successive monomorphisms, the two composites are maps between objects local for the composite monomorphism; both restrict to the identity on $e$. Proposition~\ref{cat:locality}(3) proves their equality. For the mixed law, form all the indicated pullbacks after a map into $X_2$. Lemma~\ref{rel:bc} identifies both routes with maps between objects local for the pulled-back composite monomorphism. Counit compatibility shows that their restrictions are the identity on the pulled-back input. Faithfulness of restriction again gives equality. Induction gives the finite-sequence assertion; the associativity just proved ensures that the result is independent of the induction order. \end{proof} \begin{corollary}[Coherence with prescribed loci]\label{coh:loci} Assume $\E$ is a topos. The exact isomorphism-locus formula is compatible with successive extension. For the data of Theorem~\ref{coh:successive}, if $R_0=\IsoLoc_{X_0}(e)$, then the locus after successive extension is \[ \forall_{k_2}\forall_{k_1}R_0 =\forall_{k_2k_1}R_0. \] The canonical isomorphism on any prescribed test locus agrees for successive and direct extension, and the agreement persists under arbitrary base change. \end{corollary} \begin{proof} The equality of subobjects follows from Theorem~\ref{rel:locus-formula} and uniqueness of right adjoints to composite inverse-image functors. The comparison in Theorem~\ref{coh:successive} is a map over the fixed target $B_2$. On a locus where the extended arrow is an isomorphism, the identification with the terminal slice object is unique. This gives the agreement of the specified identifications. Its stability follows from Theorem~\ref{coh:basechange} and the mixed law of Theorem~\ref{coh:successive}. \end{proof} \section{Intersections, unions, and gluing} \label{cat:lattice-section} Locality for several subobjects is governed by their intersection, while extension from a union is obtained by gluing. These formulas follow by expressing the locality functor as exponentiation by a subterminal object. Assume in this section that $\E$ is a topos, and fix $B\in\E$. Subobjects of $B$ are regarded as subterminal objects of the slice $\E/B$. For $P\hookrightarrow B$, abbreviate its locality reflector by $\Loc_P$. \begin{lemma}[Exponential description]\label{cat:exponential} For $F\in\E/B$ there is a natural isomorphism \[ \Loc_P(F)\cong F^P \] in $\E/B$. Under this isomorphism, the unit is the map that assigns to an element of $F$ its constant $P$-indexed family. \end{lemma} \begin{proof} For $H\in\E/B$ and $p:P\hookrightarrow B$, the adjunction yields \[ \Hom_B(H,\Pi_pp^*F) \cong\Hom_P(p^*H,p^*F) \cong\Hom_B(H\times_BP,F) \cong\Hom_B(H,F^P). \] The middle bijection uses the unique structure map to the subterminal $P$. Yoneda gives the isomorphism, and the image of the identity under these bijections identifies the units. \end{proof} \begin{theorem}[Normalization calculus]\label{cat:calculus} For subobjects $P,Q\hookrightarrow B$, there are canonical natural isomorphisms \begin{align} \Loc_P\Loc_Q&\cong\Loc_{P\cap Q} \cong\Loc_Q\Loc_P,\label{cat:meet}\\ \Loc_{P\cup Q}(F)&\cong \Loc_P(F)\times_{\Loc_{P\cap Q}(F)}\Loc_Q(F). \label{cat:join} \end{align} The maps in the pullback are restriction in the exponent, or equivalently the maps induced by the locality units. The first isomorphisms are compatible with permutation and parenthesization of every finite family of subobjects. All the isomorphisms commute with arbitrary pullback of $B$ and carry the corresponding unit maps to one another. \end{theorem} \begin{proof} By Lemma~\ref{cat:exponential} and the exponential law in the slice, \[ \Loc_P\Loc_Q(F)\cong(F^Q)^P \cong F^{P\times_BQ}=F^{P\cap Q}. \] The symmetry and associativity of products give the two comparisons in \eqref{cat:meet}. More explicitly, each composite represents the functor \[ H\longmapsto\Hom_B(H\times_BP_1\times_B\cdots\times_BP_n,F). \] Every comparison is induced by the canonical product comparison. Since these product comparisons have the same projections, the permutation and associativity coherence laws follow from their universal property. The description of the unit in Lemma~\ref{cat:exponential} gives its compatibility. In a topos, the union square \[ \begin{tikzcd} P\cap Q\arrow[r,hook]\arrow[d,hook]&Q\arrow[d,hook]\\ P\arrow[r,hook]&P\cup Q \end{tikzcd} \] is a pushout. Product with any $H\in\E/B$ preserves this pushout, because the slice is cartesian closed. Applying $\Hom_B(-,F)$ gives \begin{align*} \Hom_B(H,F^{P\cup Q}) \cong{}&\Hom_B(H,F^P)\\ &\mathbin{\times}_{\Hom_B(H,F^{P\cap Q})}\Hom_B(H,F^Q). \end{align*} Yoneda proves \eqref{cat:join}. Pullback preserves finite intersections and unions of subobjects in a topos, and the base-change isomorphisms for locality reflectors are those of Lemma~\ref{rel:bc}. Alternatively, each displayed comparison is characterized by its projections or evaluation map, which are preserved under pullback. This proves the final assertion. \end{proof} \begin{corollary}[Simultaneous locality]\label{cat:simultaneous} An object is both $P$-local and $Q$-local if and only if it is $(P\cap Q)$-local. If $P\subseteq Q$, every $P$-local object is $Q$-local, and \[ \Loc_P\Loc_Q\cong\Loc_P\cong\Loc_Q\Loc_P. \] \end{corollary} \begin{proof} If $F$ is $P$-local and $Q$-local, the composite unit $F\to\Loc_QF\to\Loc_P\Loc_QF$ is invertible, so Theorem~\ref{cat:calculus} makes it $(P\cap Q)$-local. Conversely, write $R=P\cap Q$. The normalization calculus gives $\Loc_P\Loc_RF\cong\Loc_RF$ and $\Loc_Q\Loc_RF\cong\Loc_RF$, compatibly with units. Hence an $R$-local object is local for both $P$ and $Q$. The final assertion is the case $P\cap Q=P$. \end{proof} There is also a version of the union formula for genuinely different families on the two pieces. Let $p:P\hookrightarrow B$, $q:Q\hookrightarrow B$, $r:R=P\cap Q\hookrightarrow B$, and $v:V=P\cup Q\hookrightarrow B$. Suppose families $E_P\to P$ and $E_Q\to Q$ are equipped with an isomorphism of their restrictions to $R$. Denote the common restricted family by $E_R\to R$ and the glued family by $E_V\to V$. Explicitly, form $E_V=E_P+_{E_R}E_Q$ over $V$ using the given overlap isomorphism. Pullback preserves this pushout. Its restriction to $P$ is $E_P+_{E_R}E_R\cong E_P$, and its restriction to $Q$ is similarly $E_Q$. Thus the glued family and its prescribed identifications exist. \begin{proposition}[Dependent-product gluing]\label{cat:gluing} There is a canonical isomorphism in $\E/B$ \[ \Pi_v(E_V)\cong \Pi_p(E_P)\times_{\Pi_r(E_R)}\Pi_q(E_Q). \] It is natural in compatible morphisms of the two families and commutes with pullback of the entire gluing diagram. \end{proposition} \begin{proof} The two maps into $\Pi_r(E_R)$ are obtained by restricting a map over $P$ or $Q$ to $R$, followed by adjunction. A map from $H\in\E/B$ into the displayed pullback is therefore a pair of maps \[ p^*H\to E_P,\qquad q^*H\to E_Q \] whose restrictions agree over $R$. The union pushout is stable under pullback. Thus $v^*H$ is obtained by gluing $p^*H$ and $q^*H$ over $r^*H$, and the pair is equivalently a map $v^*H\to E_V$. By adjunction, this is a map $H\to\Pi_v(E_V)$. The bijection is natural in $H$, proving the isomorphism. Its construction uses only restriction, adjunction, and the universal property of the union pushout. These operations are compatible with maps of the input data and with base change, proving the remaining assertions. \end{proof} \begin{remark}\label{cat:gluing-scope} The normalization and gluing results describe families in slices of a topos. Their use for equivalence extension requires the corresponding input families to satisfy the homotopical hypotheses of that extension theorem. In particular, for the glued input in Proposition~\ref{cat:gluing}, its fibration and equivalence properties must be established in the chosen homotopical setting. \end{remark} \section{Equivalence extension by dependent products}\label{hom:section} The categorical extension constructed above acquires its homotopical properties from a mapping-path argument. We give the argument explicitly, including the unit comparison that proves fibrancy of its domain. This is the dependent-product proof of equivalence extension of \cite[Proposition~116]{Awodey2023}; compare \cite{Sattler2017} and the formulation by fibred Brown factorizations in \cite[Theorem~3.3.3]{ACCRS2026}. The coherence statements in the preceding sections apply to this particular extension functor. \begin{hypothesis}[Homotopical assumptions]\label{hom:context} In addition to local cartesian closure and finite cocompleteness, assume that $\E$ has weak factorization systems \[ (\Cof,\TF),\qquad (\TC,\Fib),\qquad \TC\subseteq\Cof. \] Put $\W=\TF\circ\TC$. All four classes in a slice are defined by their underlying maps. We impose the following conditions. \begin{enumerate}[label=\textup{(P\arabic*)},leftmargin=3em] \item Cofibrations are monomorphisms, are stable under pullback, and are closed under cartesian pushout-products in every slice. \item There is an interval $I$ with endpoints $\delta_0,\delta_1:1\to I$. For every fibration $q:B\to X$, its relative path object \[ P_XB=B^{X\times I}\quad\text{in }\E/X \] has a constant-path map $c_B:B\to P_XB$, endpoint maps $p_0,p_1:P_XB\to B$ in $\TF$, and an endpoint-pair map $(p_0,p_1):P_XB\to B\times_X B$ in $\Fib$. These maps have their usual evaluation definitions, so they are preserved by change of base up to the canonical comparison isomorphisms. \item For every $X$, relative $I$-homotopy on maps between fibrant objects of $\E/X$ is an equivalence relation compatible with composition. A map between these objects lies in $\W$ if and only if it is invertible in their relative homotopy category. \end{enumerate} \end{hypothesis} Condition~\textup{(P3)} is a recognition statement restricted to fibrant objects in a slice. It does not assert the two-out-of-three property for arbitrary maps of $\E$. In the cartesian cubical setting it is established before equivalence extension in \cite[Proposition~108 and Corollary~109]{Awodey2023}. Under \textup{(P3)}, Lemma~\ref{hom:path-recognition} identifies these weak equivalences with the contractible maps defined by fibred Brown factorizations in \cite[\S3.2]{ACCRS2026}. The weak factorization systems alone imply \begin{equation}\label{hom:intersection} \TF=\Fib\cap\W. \end{equation} Indeed, if $f\in\Fib$ admits a factorization $f=pi$ with $i\in\TC$ and $p\in\TF$, lifting $i$ against $f$ exhibits $f$ as a retract of $p$. The reverse inclusion uses $\TF\subseteq\Fib$ and identity maps in $\TC$. \begin{lemma}[Dependent products and units of trivial fibrations] \label{hom:unit-tf} Let $b:B'\hookrightarrow B$ be a cofibration. \begin{enumerate}[label=\textup{(\roman*)},leftmargin=3em] \item The functor $\Pi_b:\E/B'\to\E/B$ preserves trivial fibrations. \item If $r:P\to B$ is a trivial fibration, then the unit \[ \eta_r:r\longrightarrow\Pi_b b^*r \] is a trivial fibration in $\E/B$, and hence on underlying objects. \end{enumerate} \end{lemma} \begin{proof} For (i), a lifting problem against $\Pi_b a$ is adjoint to a lifting problem against $a$ with left map obtained by pulling back along $b$. The latter is a cofibration by \textup{(P1)}. For (ii), regard $b$ as a subterminal object $B'\hookrightarrow 1_B$ of $\E/B$. In that slice the object $\Pi_b b^*r$ is canonically $P^{B'}$, and the unit is restriction $P=P^{1_B}\to P^{B'}$. For a cofibration $a$ of $\E/B$, the exponential--pushout-product adjunction identifies lifting against this restriction map with lifting $a\mathbin{\square}b$ against $P\to1_B$. The former map is a cofibration by \textup{(P1)}, and $P\to1_B$ is a trivial fibration. This proves the assertion. \end{proof} We record a categorical description of the unit square used below. It also makes explicit which slice contains each of its four objects. \begin{lemma}[A cartesian naturality square]\label{hom:unit-square} Let $b:B'\hookrightarrow B$ be a monomorphism and $r:P\to B$ any map. Write \[ P'=B'\times_B P,\qquad j:P'\hookrightarrow P,\qquad r':P'\to B'. \] Let $u:L\to P$, set $L'=j^*L$, and write $u':L'\to P'$ for its restriction. Put $t=ru$ and $t'=r'u'$. Then the pullback of \[ \Pi_b(u'):\Pi_b(t')\longrightarrow\Pi_b(r') \] along $\eta_r:r\to\Pi_b(r')$ in $\E/B$, considered as an object over $P$, is canonically $\Pi_j(u')$. Under this identification, the map from $u$ to that pullback is the unit $u\to\Pi_jj^*u$. Consequently, if this unit is invertible, the square \begin{equation}\label{hom:unit-square-display} \begin{tikzcd}[column sep=large,row sep=large] L \arrow[r,"\eta_t"] \arrow[d,"u"'] & \operatorname{dom}(\Pi_b t') \arrow[d,"\operatorname{dom}(\Pi_bu')"]\\ P \arrow[r,"\eta_r"'] & \operatorname{dom}(\Pi_b r') \end{tikzcd} \end{equation} is a pullback. In particular this holds if $u$ belongs to the essential image of $\Pi_j$. \end{lemma} \begin{proof} Test the stated pullback against an arbitrary object $a:T\to P$. A map from $T$ into it over $P$ is a map $T\to\operatorname{dom}(\Pi_b t')$ over $B$ whose composite with $\Pi_b(u')$ is $\eta_r a$. By the adjunction $b^*\dashv\Pi_b$, this is exactly a map $b^*T\to L'$ over $B'$ whose composite with $u'$ is the canonical map $b^*T\to P'$. Thus it is a map $j^*T\to u'$ in $\E/P'$. A second adjunction identifies these maps with maps $T\to\Pi_j u'$ in $\E/P$. Yoneda proves the first assertion. The induced map from $u$ corresponds under these adjunctions to the identity on $u'$, which characterizes the unit for $j^*\dashv\Pi_j$. Finally, $j$ is monic, so its counit $j^*\Pi_j\to\id$ is invertible; the unit is therefore invertible on the essential image of $\Pi_j$. \end{proof} \begin{construction}[Relative mapping paths]\label{hom:mapping-path} For a map $a:A\to B$ over $X$ with $B\to X$ a fibration, define \[ M_X(a)=A\times_{B,p_0}P_XB. \] Write $r_a:M_X(a)\to A$ and $u_a:M_X(a)\to P_XB$ for the projections, set $t_a=p_1u_a$, and define $s_a:A\to M_X(a)$ using the constant path at $a$. Then \begin{equation}\label{hom:mapping-path-identities} r_as_a=\id_A,\qquad t_as_a=a, \qquad r_a\in\TF. \end{equation} If $A\to X$ is also a fibration, then $t_a$ is a fibration: its map to $A\times_X B$ is the pullback of $(p_0,p_1)$, and the projection $A\times_X B\to B$ is a pullback of $A\to X$. All these constructions commute with change of $X$ by the canonical base-change isomorphisms for relative exponentials and pullbacks. \end{construction} \begin{lemma}[Mapping-path recognition]\label{hom:path-recognition} For a map $a:A\to B$ between fibrant objects of $\E/X$, \[ a\in\W\quad\Longleftrightarrow\quad t_a\in\TF. \] \end{lemma} \begin{proof} The three objects $A,B,M_X(a)$ are fibrant over $X$. The map $r_a$ is a trivial fibration, hence is invertible in the relative homotopy category by \textup{(P3)}. Its section $s_a$ is its inverse in that category. The identity $a=t_as_a$ therefore shows that $a$ is invertible there if and only if $t_a$ is. Apply \textup{(P3)}, the fibrancy of $t_a$, and \eqref{hom:intersection}. \end{proof} \begin{theorem}[Dependent-product equivalence extension] \label{hom:eep} Assume Hypothesis~\ref{hom:context}. Let $k:X'\hookrightarrow X$ be a cofibration, let $q:B\to X$ and $p':A'\to X'$ be fibrations, and write $B'=k^*B$, $q':B'\to X'$, and $b:B'\hookrightarrow B$. For a weak equivalence $e:A'\to B'$ over $X'$, define \begin{equation}\label{hom:eep-formula} w:\ A\longrightarrow B\ :=\Pi_b(e),\qquad p=qw. \end{equation} Then $p$ is a fibration, $w$ is a weak equivalence over $X$, and the counit identifies its restriction along $b$ with $e$. Equivalently, the restriction of $p$ along $k$ is $p'$ with its given comparison to $q'$. \end{theorem} \begin{proof} Since $b$ is monic, the counit $b^*\Pi_b(e)\cong e$ gives the restriction assertion. To prove fibrancy and weak equivalence, we first show that the mapping-path projection $t$ of $w$ is a trivial fibration. The family $p$ is then a retract of a fibration, so mapping-path recognition applies to $w$. Let $P=P_XB$ with endpoints $p_0,p_1:P\to B$. Let $P'=P_{X'}B'\cong X'\times_XP$, and let $j:P'\hookrightarrow P$. For both $\epsilon=0,1$ the square \begin{equation}\label{hom:two-endpoint-squares} \begin{tikzcd}[column sep=large,row sep=large] P' \arrow[r,hook,"j"] \arrow[d,"p'_\epsilon"'] & P \arrow[d,"p_\epsilon"]\\ B' \arrow[r,hook,"b"'] & B \end{tikzcd} \end{equation} is a pullback. Both endpoints have the same image in $X$, which is essential to using the same $j$ in these two squares. Form $M=M_X(w)$ with maps $r:M\to A$, $u:M\to P$, $s:A\to M$, and $t=p_1u:M\to B$. Restriction gives the corresponding construction $M'=M_{X'}(e)$ and maps $r',u',s',t'$. Since $e$ is a weak equivalence between fibrant objects over $X'$, Lemma~\ref{hom:path-recognition} gives \[ t':M'\longrightarrow B'\quad\text{in }\TF. \] Beck--Chevalley for \eqref{hom:two-endpoint-squares} with $\epsilon=0$ gives, as objects of $\E/P$, \begin{equation}\label{hom:local-mapping-path} u=p_0^*w=p_0^*\Pi_b(e) \cong\Pi_j\bigl((p'_0)^*e\bigr)=\Pi_j(u'). \end{equation} Now use Lemma~\ref{hom:unit-square} with $r$ in that lemma equal to $p_1:P\to B$. Equation~\eqref{hom:local-mapping-path} shows that its locality hypothesis holds, so \begin{equation}\label{hom:mapping-path-unit} \begin{tikzcd}[column sep=large,row sep=large] M \arrow[r,"\eta_t"] \arrow[d,"u"'] & \operatorname{dom}(\Pi_b t') \arrow[d,"\operatorname{dom}(\Pi_bu')"]\\ P \arrow[r,"\eta_{p_1}"'] & \operatorname{dom}(\Pi_b p'_1) \end{tikzcd} \end{equation} is a pullback. The bottom map is a trivial fibration by Lemma~\ref{hom:unit-tf}, since $p_1$ is a trivial fibration and $b$ is a cofibration. Thus $\eta_t$ is a trivial fibration. The object $\Pi_b t'$ is itself a trivial fibration by the same lemma, and the factorization \[ t=(\Pi_b t')\eta_t \] proves $t\in\TF$. Consequently $qt:M\to X$ is a fibration. The identities $rs=\id_A$, $qt=pr$, and $qts=p$ exhibit $p:A\to X$ as its retract in $\E/X$. Hence $p\in\Fib$. We may now apply Lemma~\ref{hom:path-recognition} to $w$, obtaining $w\in\W$ from $t\in\TF$. \end{proof} The restriction, normalization, base-change, and composition isomorphisms of Theorem~\ref{hom:eep} are those of the dependent-product functor established in Sections~\ref{cat:section}--\ref{cat:lattice-section}. \section{Comparison maps and their parameters} \label{cmp:section} The universe construction starts with a comparison map obtained by lifting. The comparison lemma identifies every such lift as a relative homotopy equivalence; an exponential pullback then represents all the choices in one object. \begin{lemma}[Relative comparison]\label{cmp:comparison} Assume Hypothesis~\ref{hom:context}. In a commutative square \begin{equation}\label{cmp:square} \begin{tikzcd}[column sep=large,row sep=large] A\arrow[r,"u"]\arrow[d,"v"']&C\arrow[d,"g"]\\ B\arrow[r,"f"']&D \end{tikzcd} \end{equation} suppose $u,v\in\TC$ and $f,g\in\Fib$. There is a diagonal $e:B\to C$ with $ev=u$ and $ge=f$. Every such diagonal is a weak equivalence over $D$. More precisely, it admits a homotopy inverse over $D$, and the two inverse homotopies can be chosen constant on $A$. \end{lemma} \begin{proof} The lifting property of $g$ against $v$ gives $e$. Independently, lift $u$ against $f$ to obtain $r:C\to B$ satisfying $ru=v$ and $fr=g$. For any chosen diagonal $e$, the maps $re,\id_B:B\to B$ lie over $D$ and agree after composition with $v$. The square \[ \begin{tikzcd}[column sep=large,row sep=large] A\arrow[r,"c_Bv"]\arrow[d,"v"']& P_DB\arrow[d,"{(p_0,p_1)}"]\\ B\arrow[r,"{(re,\id_B)}"']&B\times_D B \end{tikzcd} \] therefore commutes. Its right map is a fibration, so it has a diagonal $H_B:B\to P_DB$. This is a homotopy from $re$ to $\id_B$ over $D$ whose restriction to $A$ is the constant homotopy at $v$. Lifting $u$ against the endpoint-pair fibration for $P_DC$ similarly gives a homotopy from $er$ to $\id_C$, constant at $u$ on $A$. Thus $e$ is invertible in the relative homotopy category. Condition \textup{(P3)} implies that $e$ is a weak equivalence. No cancellation argument involving arbitrary weak equivalences is used. \end{proof} \begin{remark}\label{cmp:necessity} The hypotheses on $f$ and $g$ in Lemma~\ref{cmp:comparison} are essential. If its conclusion were imposed on arbitrary $f,g$, take $u=\id_A$, $v=g=t:A\to B$ and $f=\id_B$ for any $t\in\TC$. The claimed diagonal would be a two-sided inverse to $t$. Thus that stronger assertion would force every trivial cofibration to be invertible. The fibration hypotheses are present in the diagram of \cite[Lemma~121]{Awodey2023}. \end{remark} \begin{hypothesis}[Cartesian parameters]\label{cmp:cartesian} For the remainder of this section assume in addition that every object is cofibrant and that \[ a\mathbin{\square}v\in\TC \quad\text{whenever }a\in\Cof\text{ and }v\in\TC. \] For the assertions concerning cubes, also assume $\partial I=(\delta_0,\delta_1):1+1\to I$ is a cofibration. \end{hypothesis} These assumptions make the construction uniform in arbitrary parameter objects. In particular, $T\times v$ is a trivial cofibration for every $T$, by applying the mixed pushout-product condition to $\varnothing\to T$ and $v$. \begin{definition}[Object of comparison diagonals]\label{cmp:object} For the square \eqref{cmp:square}, form \[ L=C^A\times_{D^A}D^B, \qquad \lambda:C^B\longrightarrow L, \quad\lambda(e)=(ev,ge). \] The pair $(u,f)$ determines a map $\ell:1\to L$. Define \begin{equation}\label{cmp:parameter-pullback} Q=\Comp(u,v;f,g)=1\times_L C^B. \end{equation} Its representing property identifies maps $T\to Q$ with maps $e_T:B\times T\to C$ satisfying \[ e_T(v\times\id_T)=u\operatorname{pr}_A, \qquad ge_T=f\operatorname{pr}_B. \] \end{definition} \begin{theorem}[Universal comparisons and coherent parameters] \label{cmp:space} Under Hypotheses~\ref{hom:context} and \ref{cmp:cartesian}, let \eqref{cmp:square} satisfy the assumptions of Lemma~\ref{cmp:comparison}. Then: \begin{enumerate}[label=\textup{(\roman*)},leftmargin=3em] \item $Q\to1$ is a trivial fibration. In particular $Q$ has a global point, is fibrant, and all of its global points represent diagonals. \item Evaluation gives a universal comparison \[ \widehat e_Q:B\times Q\longrightarrow C\times Q \] over $D\times Q$ and under $A\times Q$. It is a weak equivalence. \item For every map $t:T\to Q$, its specialization $\widehat e_t:B\times T\to C\times T$ is a weak equivalence over $D\times T$. Specialization is compatible with identity maps and composition of parameter maps. \item For each $n\geq0$, every map $\partial I^n\to Q$ extends to $I^n\to Q$. More generally, for every $T$, every map $T\times\partial I^n\to Q$ extends to $T\times I^n\to Q$. \end{enumerate} \end{theorem} \begin{proof} For a cofibration $a$, the exponential--pushout-product adjunction gives \[ a\mathrel{\perp}\lambda \quad\Longleftrightarrow\quad a\mathbin{\square}v\mathrel{\perp}g. \] The right-hand lifting property holds because $a\mathbin{\square}v\in\TC$ and $g\in\Fib$. Consequently $\lambda\in\TF$, and its pullback $Q\to1$ lies in $\TF$. The cofibrancy of $1$ supplies a global point. The defining map $Q\to C^B$ transposes to $e_Q:B\times Q\to C$. Put $\widehat e_Q=(e_Q,\operatorname{pr}_Q)$. It is a diagonal of the product of \eqref{cmp:square} with $Q$. The two maps from $A\times Q$ are trivial cofibrations and the two maps to $D\times Q$ are fibrations. Lemma~\ref{cmp:comparison} shows that $\widehat e_Q$ is a weak equivalence. The same argument with any $T$ proves (iii); it does not require arbitrary pullbacks to preserve weak equivalences. Compatibility with parameter composition follows from the representing property of $Q$ and evaluation. Define $\partial I^0\to I^0$ to be $\varnothing\to1$, and for $n\geq1$ define the boundary inclusion by the $n$-fold pushout-product of $\partial I\to I$. These maps are cofibrations by the hypotheses. Their products with $T$ are also cofibrations, since every object is cofibrant and cofibrations are closed under pushout-products. Lifting these maps against $Q\to1$ proves (iv). \end{proof} Thus comparison diagonals form a trivially fibrant parameter object. Theorem~\ref{cmp:space} extends specified cubical boundaries of choices; selecting a point naturally in the original square is a separate requirement, addressed in Proposition~\ref{ex:graph-choice}. \section{Relative universe fillers}\label{uni:section} To fill a universe boundary, the extended family must recover the given families on both the boundary cylinder and the graph. The exact restriction theorem supplies the graph isomorphism, and cartesian realignment turns these compatible identifications into a strict boundary equality for the classifier. \begin{hypothesis}[Universes and graph boundaries]\label{uni:context} Assume Hypothesis~\ref{hom:context} and the following additional conditions. \begin{enumerate}[label=\textup{(U\arabic*)},leftmargin=3em] \item The pair $(\TC,\Fib)$ satisfies Frobenius: pulling back a trivial cofibration along a fibration gives a trivial cofibration. Every graph $\langle1_Y,j\rangle:Y\to Y\times I$, for $j:Y\to I$, belongs to $\TC$. \item For a cofibration $c:C\hookrightarrow Z$ and $i:Z\to I$, set \[ M=Z+_C(C\times I),\qquad m=c\otimes_i\delta:M\longrightarrow Z\times I, \] where the maps from $C$ are $c$ and $\langle1_C,ic\rangle$. The map $m$ is a trivial cofibration. These maps detect fibrancy: an object having the right lifting property against all such $m$ is fibrant. \item A pullback-stable class $\mathscr S$ of small fibrations is classified by a fibration $\pi:\widetilde U\to U$ in $\mathscr S$. If both input fibrations of Theorem~\ref{hom:eep} belong to $\mathscr S$, the extended fibration belongs to $\mathscr S$. \item The universe has cartesian realignment. Explicitly, for $F\to X$ in $\mathscr S$, a cofibration $j:N\hookrightarrow X$, a map $a:N\to U$, and a specified isomorphism \[ \theta_N:j^*F\xrightarrow{\cong}a^*\widetilde U, \] there are $d:X\to U$ and an isomorphism $\theta:F\xrightarrow{\cong}d^*\widetilde U$ with $dj=a$ and $j^*\theta=\theta_N$, using the prescribed pullback comparisons. \end{enumerate} \end{hypothesis} The last condition specifies both maps in a classifying square. It is the relative classification property in \cite[condition~$(2')$]{Shulman2015}; see also \cite[Definition~1.1.4, axiom~(U8)]{GSS2026}. Its formulation for underlying families permits the choice of a fibration structure to change during realignment. If structures are part of the objects being classified, the condition is instead imposed in that category of structured families. The Frobenius condition is studied in \cite{GambinoSattler2017}. In cartesian cubical sets, the graph and universe ingredients are established in \cite[\S\S3,5--8]{Awodey2023}. The descent needed here follows from the ambient categorical assumptions. \begin{lemma}[Gluing prescribed identifications]\label{uni:descent} In a finitely cocomplete locally cartesian closed category every existing pushout is stable under pullback. Let $M=X_1+_{X_0}X_2$ be such a pushout and let $F,G\in\E/M$. Isomorphisms between their restrictions to $X_1$ and $X_2$ that agree on $X_0$ glue to a unique isomorphism $F\cong G$ over $M$. \end{lemma} \begin{proof} For every $h:Y\to M$, the functor $h^*$ has the right adjoint $\Pi_h$, so $h^*$ preserves the pushout, computed in the corresponding slices. In particular, pullback along $F\to M$ writes the total object $F$ as the pushout of its restrictions to $X_1$ and $X_2$. The two given maps to $G$ therefore glue uniquely to a map over $M$. Applying the same argument to their inverses gives a map $G\to F$. Each composite is the identity on the two pieces, and hence globally, by the pushout property. This proves the assertion. \end{proof} Fix $c:C\hookrightarrow Z$ and $i:Z\to I$. A classified boundary consists of small fibrations \[ p_A:A\to C\times I,\qquad p_B:B\to Z, \] an isomorphism $\alpha:A_c\xrightarrow{\cong}c^*B$, where $A_c=\langle ic\rangle^*A$, and classifying squares with bottom maps $a:C\times I\to U$ and $b_0:Z\to U$ satisfying \[ a\langle ic\rangle=b_0c. \] The chosen classifying squares are required to induce $\alpha$. Equivalently these data come from a map $\chi:M\to U$ and its classifying family, with specified pullback representatives on the two pieces. Write $p_c:A_c\to C$. \begin{theorem}[Relative fibrancy construction]\label{uni:fibrancy} Assume Hypothesis~\ref{uni:context}. For every classified boundary there are a small fibration $p_D:D\to Z\times I$, a weak equivalence $f:D\to B\times I$ over $Z\times I$, and isomorphisms \[ \beta:(c\times I)^*D\xrightarrow{\cong}A, \qquad \gamma:\langle i\rangle^*D\xrightarrow{\cong}B \] whose comparison over $C$ is exactly $\alpha$. There is a classifying square for $D$ whose bottom map $d:Z\times I\to U$ satisfies \[ dm=\chi. \] Consequently $U$ is fibrant. \end{theorem} \begin{proof} Consider the square \begin{equation}\label{uni:comparison-square} \begin{tikzcd}[column sep=large,row sep=large] A_c\arrow[r,"{\langle1_{A_c},icp_c\rangle}"] \arrow[d,"\sigma"']&A_c\times I\arrow[d,"p_c\times I"]\\ A\arrow[r,"p_A"']&C\times I. \end{tikzcd} \end{equation} Its top map is a graph and hence a trivial cofibration. The map $\sigma$ is the pullback of the graph $\langle ic\rangle:C\to C\times I$ along $p_A$; Frobenius makes it a trivial cofibration. Both maps into $C\times I$ are fibrations: the right map is a pullback of $p_c$. Lemma~\ref{cmp:comparison} gives a weak equivalence $e_A:A\to A_c\times I$ over $C\times I$ and under $A_c$. Consequently \[ e=(\alpha\times I)e_A:A\longrightarrow(c^*B)\times I \] is a weak equivalence whose graph restriction is the specified isomorphism $\alpha$. Composition with an isomorphism preserves $\W=\TF\circ\TC$, independently of two-out-of-three. Let $B'=c^*B$ and let $b:B'\hookrightarrow B$ be the pullback of $c$. Apply Theorem~\ref{hom:eep} with base inclusion $c\times I$ and put \begin{equation}\label{uni:dependent-product} f=\Pi_{b\times I}(e):D\longrightarrow B\times I, \qquad p_D=(p_B\times I)f. \end{equation} The theorem gives the fibration and weak-equivalence assertions, and \textup{(U3)} gives smallness. The counit supplies $\beta$. Apply Theorem~\ref{rel:exact} to the test map $\langle i\rangle:Z\to Z\times I$. The input restriction is $\alpha$, so the graph restriction of $f$ is an isomorphism. Identifying the graph restriction of $B\times I$ with $B$, use this actual restricted map as $\gamma$. Counit compatibility gives the identity \begin{equation}\label{uni:boundary-identity} c^*\gamma=\alpha\,\langle ic\rangle^*\beta \end{equation} after the canonical interchange of pullbacks. In total-space terms the same conclusion is the calculation \[ \langle1_B,ip_B\rangle^*f\cong\Pi_b(\alpha), \] whose right side is terminal in $\E/B$. The specified classifying squares for $A$ and $B$, together with $\beta,\gamma$ and \eqref{uni:boundary-identity}, give compatible isomorphisms between $m^*D$ and $\chi^*\widetilde U$ on the two pieces of $M$. Lemma~\ref{uni:descent} gives a specified global isomorphism \[ \theta_M:m^*D\xrightarrow{\cong}\chi^*\widetilde U. \] Apply cartesian realignment to $(D,m,\chi,\theta_M)$. It produces the asserted classifying square and the strict equality $dm=\chi$. Finally every lifting problem against a map $m$ determines just such a classified boundary by pulling back $\pi$. Condition~\textup{(U2)} therefore proves fibrancy of $U$. \end{proof} For a chosen comparison $e_A$, every categorical comparison in this proof is the one established in Sections~\ref{rel:section} and \ref{coh:section}. The first choice can also be retained as a parameter. \begin{theorem}[A family of universe fillers]\label{uni:parameter} Assume Hypotheses~\ref{uni:context} and \ref{cmp:cartesian}. For a fixed classified boundary $\xi$, let $Q_\xi$ be the comparison object for \eqref{uni:comparison-square}. Then $Q_\xi\to1$ is a trivial fibration, and there exist a small fibration \[ D_\xi\longrightarrow Z\times I\times Q_\xi \] and a classifying map \[ d_\xi:Z\times I\times Q_\xi\longrightarrow U \] with the following properties. \begin{enumerate} \item Its restrictions to $(C\times I)\times Q_\xi$ and to $Z\times Q_\xi$ along the graph of $i$ have specified canonical identifications with the constant parameter families $A\times Q_\xi$ and $B\times Q_\xi$, with identification $\alpha\times\id_{Q_\xi}$. \item The boundary equality is strict: \[ d_\xi(m\times\id_{Q_\xi})=\chi\operatorname{pr}_M. \] \item For every $t:T\to Q_\xi$, the pulled-back family is canonically the dependent-product extension of the comparison represented by $t$. These identifications respect all composites of parameter maps. The corresponding classifying map is $d_\xi(\id_{Z\times I}\times t)$. \item Every map $h:T\times\partial I^n\to Q_\xi$ extends to $\bar h:T\times I^n\to Q_\xi$. Composing $\bar h$ with $d_\xi$ gives a compatible extension of the resulting family of universe fillers, relative to the fixed boundary classifier $\chi$. \end{enumerate} \end{theorem} \begin{proof} Theorem~\ref{cmp:space} gives $Q_\xi$ and the universal weak equivalence \[ e_{A,Q}:A\times Q_\xi\longrightarrow A_c\times I\times Q_\xi \] over $C\times I\times Q_\xi$, under $A_c\times Q_\xi$. Compose it with $\alpha\times\id_{I\times Q_\xi}$ and apply Theorem~\ref{hom:eep} along $(c\times I)\times\id_{Q_\xi}$. The resulting arrow is the dependent product along $(b\times I)\times\id_{Q_\xi}$. Its domain family is small by \textup{(U3)}. Theorem~\ref{rel:exact} gives the graph isomorphism, including the specified comparison $\alpha\times\id_{Q_\xi}$. Product with $Q_\xi$ preserves the boundary pushout, and $m\times\id_{Q_\xi}$ is a cofibration. Repeat the descent and cartesian realignment step of Theorem~\ref{uni:fibrancy} once over this product boundary. This gives $d_\xi$ with the strict equality in (ii). For $t:T\to Q_\xi$, Theorem~\ref{coh:basechange} identifies the specialization with dependent-product extension of the specialized comparison. Theorem~\ref{cmp:space} verifies that this comparison is a weak equivalence, without invoking pullback stability for arbitrary weak equivalences. The coherence laws in Theorem~\ref{coh:basechange} give the compatibility of these identifications; compatibility of the displayed classifying maps follows by composition of actual maps. Finally, lift $T\times\partial I^n\to Q_\xi$ against the trivial fibration $Q_\xi\to1$. Composing with $d_\xi$ proves (iv), and (ii) makes this construction relative to $\chi$. \end{proof} The parameter theorem gives one family after a realignment has been chosen for the fixed boundary $\xi$. It retains all comparison choices inside that family. Its cubical extension statement is about comparison-parameterized families of fillers. A natural point of $Q_\xi$, or a natural choice of realignment as $\xi$ varies, is an additional structure. The finite-groupoid example below distinguishes these requirements. \begin{theorem}[The space of strict universe fillers]\label{uni:all-fillers} Assume Hypotheses~\ref{uni:context} and \ref{cmp:cartesian}. Fix a classified boundary $\xi$ with classifier $\chi:M\to U$, and put $X=Z\times I$, so that $m:M\to X$ is its boundary inclusion. Let $\ulcorner\chi\urcorner:1\to U^M$ be the transpose of $\chi$, and define $H_\chi$ by the pullback square \begin{equation}\label{uni:all-fillers-pullback} \begin{tikzcd}[column sep=large,row sep=large] H_\chi\arrow[r]\arrow[d]&U^X\arrow[d,"U^m"]\\ 1\arrow[r,"\ulcorner\chi\urcorner"']&U^M. \end{tikzcd} \end{equation} Then the following assertions hold. \begin{enumerate} \item Maps $T\to H_\chi$ correspond naturally to maps $d:X\times T\to U$ satisfying \[ d(m\times\id_T)=\chi\operatorname{pr}_M. \] Thus $H_\chi$ represents all strict fillers of the fixed boundary. \item The map $H_\chi\to1$ is a trivial fibration. For every object $T$ and every $n\geq0$, a family of strict fillers parameterized by $T\times\partial I^n$ extends to one parameterized by $T\times I^n$, preserving the boundary equality. \item The classifying map $d_\xi$ of Theorem~\ref{uni:parameter} induces a map \[ \Phi_\xi:Q_\xi\longrightarrow H_\chi. \] Every such map arising from a choice of the realignment in that theorem is a weak equivalence. \end{enumerate} \end{theorem} \begin{proof} The exponential adjunction and the defining pullback give (i), including its naturality in $T$. By Theorem~\ref{uni:fibrancy}, $U\to1$ is a fibration. For any cofibration $a$, the exponential--pushout-product adjunction identifies lifting $a$ against $U^m$ with lifting $a\mathbin{\square}m$ against $U\to1$. The map $m$ is a trivial cofibration, so the mixed pushout-product hypothesis makes $a\mathbin{\square}m$ a trivial cofibration. Therefore $U^m\in\TF$. Its pullback $H_\chi\to1$ also belongs to $\TF$. The maps $\partial I^n\to I^n$ are cofibrations, including $\partial I^0\to I^0=\varnothing\to1$. Their products with $T$ are cofibrations as well. A lifting problem against $H_\chi\to1$ extends any map $T\times\partial I^n\to H_\chi$ to $T\times I^n\to H_\chi$. The representing property in (i) translates this extension into the asserted family of strict fillers. The strict boundary equality for $d_\xi$ makes its transpose factor through the pullback \eqref{uni:all-fillers-pullback}, giving $\Phi_\xi$. Both $Q_\xi\to1$ and $H_\chi\to1$ are trivial fibrations, and hence their domains are fibrant. In the relative homotopy category over $1$, their classes are invertible by \textup{(P3)}. The identity \[ (H_\chi\to1)\,\Phi_\xi=(Q_\xi\to1) \] therefore makes $[\Phi_\xi]$ invertible. Applying \textup{(P3)} again shows that $\Phi_\xi\in\W$. This argument uses the homotopy category of fibrant objects and applies to every permitted choice of $d_\xi$. \end{proof} \begin{remark}\label{uni:all-fillers-scope} Theorem~\ref{uni:all-fillers} includes strict classifiers obtained from different choices of comparison and realignment for the fixed boundary. For example, any two such classifiers are joined by an $I$-parameter family through strict fillers, and every specified cubical boundary of these families extends. These statements concern the maps into $U$ with their fixed boundary value. Additional prescribed identifications of their total families would be additional data, and the theorem does not choose a point of $H_\chi$ naturally as the boundary $\chi$ varies. \end{remark} \section{Smallness and model recognition}\label{size:section} We make the size condition in \textup{(U3)} explicit in a presheaf topos. Let $\E=\Set^{\mathcal A^{\mathrm{op}}}$, where $\mathcal A$ is small. A map $p:F\to X$ is \emph{$\kappa$-small} if each set-theoretic fibre of $p_a:F(a)\to X(a)$ has cardinality less than $\kappa$. \begin{proposition}[Smallness of dependent-product extension] \label{size:bound} Let $\kappa$ be strongly inaccessible and larger than the cardinality of the set of arrows of $\mathcal A$. Let $k:X'\hookrightarrow X$ be a monomorphism and set $b:X'\times_XB\hookrightarrow B$. If $q:B\to X$ and $p':A'\to X'$ are $\kappa$-small and $e:A'\to X'\times_XB$ lies over $X'$, then the family \[ p=q\Pi_b(e):A\longrightarrow X \] is $\kappa$-small. This statement is independent of fibrancy and weak equivalence. \end{proposition} \begin{proof} Fix $a\in\mathcal A$ and $x\in X(a)$. A point of the fibre of $A(a)\to X(a)$ first chooses $y\in B(a)_x$. The fibre of $\Pi_b(e)$ over $y$ is the set of sections of the restricted family over the pullback of $B'\hookrightarrow B$ along $y:\mathcal A(-,a)\to B$. Such a section is a compatible collection indexed by arrows $\alpha:d\to a$ for which $B(\alpha)y$ belongs to $B'(d)$. There are fewer than $\kappa$ such arrows. For each index, the available values belong to \[ e_d^{-1}(B(\alpha)y), \] a subset of a fibre of $p'_d$, of cardinality less than $\kappa$. The compatibility equations cut out a subset of their product. Strong inaccessibility bounds that product by a cardinal less than $\kappa$, including the empty product. There are fewer than $\kappa$ possible $y$, and regularity bounds their disjoint union by a cardinal less than $\kappa$. This proves the claim for every $a,x$. \end{proof} \begin{corollary}[Size-indexed fibrant universes]\label{size:universes} Suppose the homotopical and graph assumptions above hold in the presheaf topos, and for each $\kappa$ in a collection $\mathcal K$ of cardinals as in Proposition~\ref{size:bound} there is a universe $\pi_\kappa:\widetilde U_\kappa\to U_\kappa$ for the $\kappa$-small fibrations with cartesian realignment. Then every $U_\kappa$ is fibrant, and every $\kappa$-small fibration extends, still $\kappa$-small, along every trivial cofibration. If every fibration is $\kappa$-small for some $\kappa\in\mathcal K$, all fibrations have the extension property. \end{corollary} \begin{proof} Proposition~\ref{size:bound} verifies the extension-smallness clause of \textup{(U3)}. Theorem~\ref{uni:fibrancy} proves fibrancy of each $U_\kappa$. For a classified fibration $F\to Y$ and a trivial cofibration $j:Y\to Z$, extend its classifier $Y\to U_\kappa$ across $j$ by fibrancy. Pulling back $\pi_\kappa$ gives the required extension, with the chosen comparison on $Y$. For the last assertion choose an admissible $\kappa$ separately for each fibration. No single universe for families of unbounded size is required. \end{proof} \begin{proposition}[Verification of the model recognition conditions] \label{size:recognition} Hypothesis~\ref{hom:context} implies the following statements. \begin{enumerate} \item In a commuting triangle $A\to Y\to X$ with $A\to Y$ and $A\to X$ in $\TC$ and $f:Y\to X$ in $\Fib$, the map $f$ belongs to $\TF$. \item Within the subcategory of fibrations, trivial fibrations satisfy two-out-of-three. \item Trivial fibrations extend along every cofibration. \end{enumerate} \end{proposition} \begin{proof} For (i), apply Lemma~\ref{cmp:comparison} to the square with top $A\to X$, left side $A\to Y$, bottom $f:Y\to X$, and right side $\id_X$. Its diagonal is necessarily $f$. Hence $f\in\W$, and \eqref{hom:intersection} gives $f\in\TF$. For (ii), a composable pair of fibrations $A\to B\to C$ gives three fibrant objects of $\E/C$. By \textup{(P3)}, the weak equivalences between them are exactly the isomorphisms in their relative homotopy category, which satisfy two-out-of-three. All three maps are fibrations, so \eqref{hom:intersection} gives the assertion for trivial fibrations. For (iii), let $j:Y\hookrightarrow Z$ be a cofibration and $p:F\to Y$ a trivial fibration. By Lemma~\ref{hom:unit-tf}(i), the object $\Pi_j(p)$ is a trivial fibration over $Z$. Since $j$ is monic, its counit identifies the restriction with $p$. \end{proof} \begin{corollary}[Model structure from cofinal universes] \label{size:model} Under the hypotheses of Corollary~\ref{size:universes}, suppose every fibration is classified at some level in $\mathcal K$. Then $\W=\TF\circ\TC$ satisfies two-out-of-three, and $(\Cof,\W,\Fib)$ is a right proper model structure. \end{corollary} \begin{proof} Corollary~\ref{size:universes} gives extension of all fibrations along trivial cofibrations. Proposition~\ref{size:recognition} verifies the span property, the relative two-out-of-three condition for trivial fibrations, and extension of trivial fibrations. Frobenius is part of \textup{(U1)}. These are precisely the hypotheses of \cite[Theorem~2.8]{Sattler2017}, which gives the asserted model structure and right properness. The ambient presheaf topos has all small limits and colimits. \end{proof} \section{Examples and the limits of natural choice}\label{sec:examples} The coherence of dependent-product extension concerns an operation on a specified arrow. The comparison arrow used to produce the input to that operation may involve a choice of lift. The following example distinguishes these two statements within the usual Kan--Quillen model category. \begin{proposition}[An obstruction to natural graph comparison]\label{ex:graph-choice} There is no choice of graph-comparison maps that is natural under all isomorphisms of the underlying graph data, even for diagrams consisting of nerves of finite groupoids in simplicial sets. \end{proposition} \begin{proof} For a nonempty finite set $S$, let $\mathbb J(S)$ be the groupoid with object set $S$ and exactly one morphism between every ordered pair of objects. Its nerve $N\mathbb J(S)$ is a contractible Kan complex. Set \[ I=N\mathbb J(\{0,1\}),\qquad A=N\mathbb J(\{a,b,c\}), \] and let $p:A\to I$ be induced by $p(a)=p(b)=0$ and $p(c)=1$. The underlying functor is an isofibration: an isomorphism with source $p(x)$ can be lifted to the unique isomorphism from $x$ to any object over its target. Consequently $p$ is a Kan fibration. Its fibre at $0$ is \[ A_0=N\mathbb J(\{a,b\}). \] Both $A_0\hookrightarrow A$ and $A_0\times\{0\}\hookrightarrow A_0\times I$ are monomorphisms and weak equivalences. Thus Lemma~\ref{cmp:comparison} applies, and there exist maps \[ e:A\longrightarrow A_0\times I \quad\text{over }I,\qquad e|_{A_0}=\langle\id_{A_0},0\rangle. \] For example, the functor that sends $c$ to $(a,1)$ and sends $a,b$ to $(a,0),(b,0)$ respectively induces such a map. Every such map is a weak equivalence, since its source and target are nonempty contractible Kan complexes. Let $\sigma:A\to A$ interchange $a,b$ and fix $c$. This is an automorphism over $I$, and it induces the transposition $\sigma_0:A_0\to A_0$ on the fibre. Naturality under this automorphism would require \begin{equation}\label{eq:graph-equivariance-obstruction} e\sigma=(\sigma_0\times\id_I)e. \end{equation} At the vertex $c$, the left-hand side is $e(c)$, whereas the right-hand side interchanges the two possible values $(a,1)$ and $(b,1)$ of $e(c)$. Equation~\eqref{eq:graph-equivariance-obstruction} is therefore impossible. \end{proof} \begin{remark}\label{ex:scope-natural-choice} Proposition~\ref{ex:graph-choice} concerns naturality under isomorphisms of the full unstructured input, including automorphisms of the total fibration. It makes no assertion that a chosen operation cannot be stable under base substitution alone. It also permits natural lifting operations on categories whose morphisms preserve specified lifting structure. Once the comparison arrow $e$ is part of the input, the dependent-product construction applies functorially to that input and has the coherence established above. Strictification by passage to a split comprehension category is a further operation; the local universes construction of \cite{LumsdaineWarren2015} provides a general coherence theorem of that kind for weakly stable type-theoretic structure. \end{remark} \begin{example}[Classifying maps and specified identifications]\label{ex:weak-realignment} Consider the arrow topos $\E=\mathrm{Set}^{[0\to1]}$. Write its objects as maps $S_0\to S_1$, and put \[ K=(\{*\}\longrightarrow\{0,1\}),\qquad *\longmapsto0, \qquad U=1_{\E},\qquad \widetilde U=K. \] Let $\mathscr S$ consist of all families isomorphic to projections $X\times K\to X$. This is a pullback-stable class of families classified by $\pi:K\to1_{\E}$. Any condition asking only for extension of the bottom classifying map holds: that map is the unique map to $1_{\E}$. Take \[ M=(\varnothing\longrightarrow\{*\}) \hookrightarrow X=(\{*\}\longrightarrow\{*\})=1_{\E}. \] The restriction of $K\to X$ is $(\varnothing\to\{0,1\})\to M$. Interchanging $0,1$ gives an automorphism $\theta_M$ of this restricted family, hence a specified cartesian identification with the pullback of $\pi$. It cannot be the restriction of an automorphism of $K$: naturality with respect to the map $\{*\}\to\{0,1\}$ forces the second component of any such automorphism to fix $0$, and hence to be the identity. Thus extension of bottom classifying maps does not in general imply extension of a prescribed cartesian identification. This example concerns categorical families and isolates the strength of cartesian realignment. Realignment in the sense of a specified cartesian square, as in Shulman's condition $(2')$ \cite{Shulman2015} and the universe axioms of \cite{GSS2026}, includes the additional identification data. \end{example} \begin{example}[An equivalence-extension witness need not be normalized] \label{ex:unnormalized-eep} In simplicial sets, let $k:\varnothing\hookrightarrow\Delta^0$, let $q:\Delta^0\to\Delta^0$ be the identity, and use the boundary equivalence $e:\varnothing\to\varnothing$. Let $K=N\mathbb J(\{0,1\})$. The map \[ K\longrightarrow\Delta^0 \] is a weak equivalence between fibrant objects and is itself a Kan fibration. Its restriction along $k$ is the given boundary equivalence, so it is a valid equivalence-extension witness. It is not an isomorphism, since $K$ has two vertices. By contrast, dependent-product extension along the empty subobject gives $\id_{\Delta^0}$, because the relevant right adjoint sends the terminal object of $\mathrm{sSet}/\varnothing$ to the terminal object of $\mathrm{sSet}/\Delta^0$. Normalization is therefore a property of the specified dependent-product construction; an arbitrary equivalence-extension witness need not satisfy it. \end{example} \begin{example}[The isomorphism locus in a non-Boolean topos] \label{ex:sierpinski-locus} Let $S=\{0,1\}$ have open subsets $\varnothing$, $\{1\}$, and $S$, and work in $\E=\mathrm{Sh}(S)$. Write $V\hookrightarrow1$ for the subterminal corresponding to the open set $\{1\}$. The three subobjects of $1$ form the Heyting algebra \[ 0