1. Question, contribution, and conventions
We extend Patterson's initial-functor semantics [1] to proof spaces and models in an infinity-topos. The results synthesize established higher category theory with explicit soundness and exactness arguments. The PDF and source supplement expand the discussion.
An $\infty$-category means an $(\infty,1)$-category. Its mapping objects are spaces; morphisms of dimension at least two are invertible. Write $\mathcal S$ for spaces, $|A|=\operatorname{colim}_A *$ for groupoid completion, and $\tau_{\leq n}$ for truncation. All indexing categories are small relative to fixed universes. Limits, colimits, and commutative diagrams are homotopy coherent. “Cartesian” means finite-product-preserving; it does not mean finite-limit-preserving. We distinguish this usage from cartesian fibrations.
For $u:A\to B$, set $A_{/b}=A\times_B B_{/b}$, the comma $\infty$-category of arrows $u(a)\to b$. Call $u$ initial when $|A_{/b}|\simeq *$ for every $b$. This is the convention appropriate to limits, also called left cofinal [4]. Initiality is stronger than an equivalence after groupoid completion.
The left fibration $\int_B Y\to B$ classified by $Y:B\to\mathcal S$ has fiber $Y(b)$ and covariant transport. This variance is essential: limits are computed by sections of left fibrations, whereas their classification uses covariant functors.
2. The cartesian Kan-extension theorem
Lemma 2.1 (Products in the elements construction). If $C$ has finite products and $X:C\to\mathcal S$ preserves them, then $E=\int_C X$ has finite products. The projection $p:E\to C$ preserves and reflects product cones.
Proof. For finitely many $(c_i,x_i)$, choose $c=\prod_i c_i$. The equivalence $X(c)\simeq\prod_i X(c_i)$ gives a contractible space of lifts of the tuple $(x_i)$, including its comparison paths. These data define the product cone. To check its universal property, for any $(d,z)$ the space of arrows to $(c,x)$ is the homotopy fiber, over $x$, of $$ \operatorname{Map}_C(d,c)\longrightarrow X(c),\qquad f\longmapsto X(f)(z). $$ The product comparisons identify this fiber with the product of the corresponding fibers for $(c_i,x_i)$. For the empty family, $X(1_C)\simeq *$. The same calculation shows that any cone projecting to a product cone is a product cone. $\square$
Lemma 2.2 (Homotopy cosiftedness). If $E$ has finite products, then $E^{\mathrm{op}}$ is sifted in the $\infty$-categorical sense.
Proof. It has an initial object and finite coproducts. For a pair of objects, its category of common targets has the coproduct cocone as an initial object, hence contractible groupoid completion. The siftedness criterion [5] applies. Equivalently, each finite diagonal is final because it has a left adjoint. Thus colimits of this shape in spaces commute with finite products. Connectedness alone would not suffice here. $\square$
Theorem 2.3 (Product-preserving Kan extensions). Let $C,D$ be small cartesian $\infty$-categories, let $X:C\to\mathcal S$ preserve finite products, and let $F:C\to D$ be any functor. Then $\operatorname{Lan}_F X$ preserves finite products. No product-preservation assumption on $F$ is required.
Proof. Covariant density and the Yoneda lemma give $$ X\simeq\operatorname{colim}_{(c,x)\in(\int_C X)^{\mathrm{op}}} \operatorname{Map}_C(c,-), $$ and therefore $$ \operatorname{Lan}_F X\simeq \operatorname{colim}_{(c,x)\in(\int_C X)^{\mathrm{op}}} \operatorname{Map}_D(Fc,-). \tag{1} $$ Indeed, left Kan extension takes the displayed covariant representable to $\operatorname{Map}_D(Fc,-)$ by its defining adjunction. Each summand preserves products. Lemmas 2.1 and 2.2 make the indexing category sifted, so its colimit preserves finite products, including the terminal object. $\square$
This proof is the space-valued analogue of the classical argument associated with Borceux and Day [2]. Its essential replacement is homotopy siftedness rather than ordinary siftedness. The ambient density and sifted-completion results are standard [3, Sections 5.1 and 5.5.8].
Corollary 2.4 (Topos-valued form). Theorem 2.3 holds with any $\infty$-topos $\mathcal X$ in place of $\mathcal S$.
Proof. Present $\mathcal X$ as an accessible left exact localization $L:\mathcal P(K)\rightleftarrows\mathcal X:i$. The right adjoint $i$ preserves products. Evaluate $iX$ at each object of $K$ and apply Theorem 2.3; the pointwise left Kan extension in $\mathcal P(K)$ preserves products. Applying the product-preserving left adjoint $L$ gives the left Kan extension in $\mathcal X$. This follows from $LiX\simeq X$ and the Kan-extension adjunction. $\square$
3. Cartesian comprehensive factorization
Let $\mathrm{Cart}_\infty$ have small cartesian $\infty$-categories as objects and product-preserving functors as morphisms. An orthogonal factorization system here means that every morphism factors into the two classes and each compatible lifting problem has a contractible space of fillers.
Theorem 3.1. The initial/left-fibration factorization system on $\mathrm{Cat}_\infty$ restricts to $\mathrm{Cart}_\infty$. Explicitly, for a cartesian $F:C\to D$, put $$ Y_F(d)=\operatorname{colim}_{(c,Fc\to d)\in C_{/d}} * =|C_{/d}|, \qquad E_F=\int_D Y_F. $$ There is a factorization $C\xrightarrow{\eta_F}E_F\xrightarrow{p_F}D$, with $\eta_F$ initial, $p_F$ a left fibration, and both functors cartesian. It is unique up to contractible choice within the factorization system.
Proof. The higher comprehensive factorization is standard [6, Section 7.4]; the displayed construction is its covariant Kan-extension description. Namely $Y_F=\operatorname{Lan}_F1_C$, and the unit supplies $\eta_F$ over $D$. The defining universal property is $$ \operatorname{Map}_{/D}(E_F,\textstyle\int_D Z) \simeq \operatorname{Nat}(Y_F,Z) \simeq \operatorname{Nat}(1_C,ZF) \simeq \operatorname{Map}_{/D}(C,\textstyle\int_D Z) $$ for every $Z:D\to\mathcal S$. This is the left-fibration reflection underlying comprehensive factorization.
Theorem 2.3 makes $Y_F$ cartesian. Lemma 2.1 makes $E_F$ cartesian and makes $p_F$ preserve and reflect products. Since $p_F\eta_F\simeq F$ preserves products, reflection implies that $\eta_F$ does too.
For completeness, orthogonality restricts as well. A left fibration $p:E\to D$ between cartesian categories that preserves products has a product-preserving classifier: its product cones identify the fibers over $\prod d_i$ with the product of the fibers over $d_i$, including the empty case. Lemma 2.1 then shows that $p$ reflects product cones. In a lifting square of cartesian functors, the ambient filler $h$ has $ph$ cartesian; hence $h$ is cartesian. Consequently the space of cartesian fillers is the same contractible space as the ambient one. Closure under retracts and the ambient characterization of the two classes finish the restriction. $\square$
The ordinary discrete-opfibration factor is recovered from the classifier $d\mapsto\pi_0|C_{/d}|$, since $\pi_0$ preserves colimits and products [7].
4. Solutions and levels of observational equality
Fix a cartesian $\infty$-category $T$ and a model $M:T\to\mathcal X$ preserving products. A higher term diagram is a cartesian $D:J\to T$. Its solution object is $$ \operatorname{Sol}_M(D)=\lim_{j\in J}MD(j). $$ A transformation consists of a cartesian $u:J\to K$ and a specified equivalence $D\simeq D'u$. Its comparison on solutions goes in the reverse direction. Points of a solution object include compatible values and all required coherence; merely solving equations in the homotopy category loses this information.
Theorem 4.1 (Soundness). If $u$ is initial, its comparison on solutions is an equivalence. A zigzag of such transformations preserves the solution object up to equivalence.
Proof. Apply the initial-functor theorem to $MD'$. Alternatively, apply every generalized-point functor $\operatorname{Map}_{\mathcal X}(U,-)$, use the space-valued theorem, and invoke Yoneda. Compose the resulting equivalences along the zigzag. $\square$
Definition 4.2. For $n\geq0$, call $u:A\to B$ $n$-initial if $\tau_{\leq n}|A_{/b}|\simeq *$ for every $b$. This definition measures the truncation level of observations; it does not assert a separate factorization system for every $n$.
Theorem 4.3 (Exact truncation criterion). The following are equivalent:
1. $u$ is $n$-initial. 2. For every $H:B\to\mathcal S_{\leq n}$, restriction induces an equivalence $\lim_B H\simeq\lim_A Hu$.
They imply the same statement for diagrams of $n$-truncated objects in any $\infty$-topos, and in any of its slices.
Proof. In $\operatorname{Fun}(B,\mathcal S_{\leq n})$, the left Kan extension of the terminal diagram is $$ Y_n(b)=\tau_{\leq n}\operatorname{colim}_{A_{/b}}*=\tau_{\leq n}|A_{/b}|. $$ Restriction on limits is the map $$ \operatorname{Map}(1_B,H)\longrightarrow\operatorname{Map}(Y_n,H) $$ induced by $Y_n\to1_B$, using the Kan-extension adjunction. It is an equivalence for every $H$ exactly when $Y_n\to1_B$ is an equivalence, by Yoneda. Generalized points of an $n$-truncated object are $n$-truncated spaces and preserve limits, proving the topos and slice assertions. $\square$
Thus $0$-initiality recovers the nonempty-connected comma criterion of ordinary category theory, while full initiality requires contractibility. This distinction is already visible for $B G\to *$, where $G$ is a nontrivial discrete group. It is $0$-initial, but the comparison $BG\to\operatorname{Map}(BG,BG)$ for the constant diagram with value $BG$ is not an equivalence: its image consists of constant maps, and the identity is not null-homotopic. This example concerns general indexing categories; $BG$ is not being presented as a cartesian category.
5. Proof spaces and the lens calculation
For a fixed context $\Gamma$ and output sort $A$, terms belong to a mapping space $\operatorname{Map}_T(\Gamma,A)$. A chosen rewrite becomes a path in that space. Rewriting inside an operation or substitution is induced by composition and finite products. A path between parallel derivations is a two-dimensional coherence in the mapping space, hence one dimension higher than a rewrite. Directed reductions can instead be retained in an $(\infty,2)$-categorical presentation; passing to equality semantics inverts them.
For a finite represented fragment, form the realization of its term-and-rewrite graph $G$ and attach cells for specified comparisons between derivations. Operations and substitution require additional compatible structure; polygraphs provide a framework [8]. This is not a complete saturation algorithm.
Proposition 5.1 (Congruence does not determine coherence). The set $\pi_0|G|$ is the equivalence closure of the edges of $G$. It does not determine the homotopy type of a proof space, even for finite presentations.
Proof. Two vertices lie in the same component exactly when joined by a finite unoriented edge path. Consider vertices $s,a,b,t$ with edges $s\to a\to t$ and $s\to b\to t$. Their realization is a circle. Attaching a disk along the diamond yields a contractible space. Both have one component, but their fundamental groups are $\mathbb Z$ and $0$. Attaching cells of dimension at least two never changes components. Hence equality of classes cannot certify equality of proof spaces. $\square$
The lens example admits a particularly explicit witness. In the internal language of $\mathcal X$, suppose maps $g:S\to V$, $p:S\times V\to S$ come with homotopies $$ \alpha_{s,v}:g(p(s,v))=v, \qquad \beta_s:p(s,g(s))=s. $$ Concatenation $r\cdot q$ means first $r$, then $q$.
Proposition 5.2 (Witnessed PutTwice). There is a specified homotopy $$ \delta_{s,v}:p(p(s,v),v)=p(s,v), \qquad \delta_{s,v}=\bigl(\operatorname{ap}_{p(p(s,v),-)}\alpha_{s,v}\bigr)^{-1} \cdot\beta_{p(s,v)}. \tag{2} $$
Proof. Put $x=p(s,v)$. Applying $p(x,-)$ to $\alpha_{s,v}$ gives a path from $p(x,g(x))$ to $p(x,v)$. Reverse this path and concatenate with $\beta_x:p(x,g(x))=x$. The endpoints are exactly those in (2). Path functoriality makes the construction natural in $(s,v)$. $\square$
The witness need not be unique and does not prove PutPut for distinct views. The supplement gives a three-state model satisfying PutGet, GetPut, and PutTwice but failing PutPut.
6. Topos semantics, substitution, and descent
An $\infty$-topos is an accessible left exact localization of a presheaf $\infty$-category. Its slices interpret parameter contexts and its $0$-truncated objects form an ordinary topos. Models $\operatorname{Fun}^{\times}(T,\mathcal X)$ need not themselves form a topos: pointed spaces are a nontrivial example with initial and terminal objects equal, impossible in a nontrivial $\infty$-topos. No arbitrary localization of term diagrams is asserted to be left exact.
Proposition 6.1 (Parameterized soundness). For $M:T\to\mathcal X_{/U}$, initial transformations preserve $\operatorname{Sol}_M(D)$ in the slice. If $f:V\to U$, then $$ f^*\operatorname{Sol}_M(D)\simeq\operatorname{Sol}_{f^*M}(D). \tag{3} $$ Theorem 2.3 also applies to Kan extension with values in $\mathcal X_{/U}$.
Proof. The slice is an $\infty$-topos. Apply Theorem 4.1 and Corollary 2.4 there. Pullback $f^*$ has both a left adjoint $\Sigma_f$ and a right adjoint $\Pi_f$, so it preserves limits and colimits; preservation of the defining limit proves (3). $\square$
For a more concrete constraint language, suppose $A\to U$ is a family of assignments and $r,s:A\rightrightarrows B$ are maps over $U$. The family of assignments with an equality witness is the homotopy pullback $$ \operatorname{Eq}(r,s)=A\times_{B\times_U B}B, $$ using $(r,s)$ and the diagonal of $B$. Its fiber is the identity type $r(a)=s(a)$. Further constraints between proofs are formed by iterating this construction. Finite systems use finite limits and hence are preserved by inverse-image functors of geometric morphisms. Arbitrary infinite limits need not be so preserved; this statement is distinct from the all-limit preservation of pullback between slices in (3).
Proposition 6.2 (Descent for witnesses). If $q:U'\to U$ is an effective epimorphism with Cech nerve $U'_\bullet$, and $Z\to U$ is any solution family, then $$ \operatorname{Map}_{\mathcal X_{/U}}(U,Z) \simeq\lim_{[k]\in\Delta} \operatorname{Map}_{\mathcal X_{/U}}(U'_k,Z). \tag{4} $$ Equivalences between solution families can be checked after pullback along $q$.
Proof. Effectiveness expresses $U$ as the colimit of its Cech nerve in the slice. Mapping into $Z$ changes this colimit to the limit (4). Descent identifies the slice over $U$ with compatible families over that nerve, and therefore makes pullback along $q$ conservative. $\square$
Local witnesses therefore require coherent overlap data to descend. Internal comprehensive factorization is already established in [6, Corollary 7.23]; we do not claim an additional internal product-restriction or dependent-syntax completeness theorem.
7. Exactness boundaries and a finite-limit criterion
Proposition 7.1 (Truncation is not left exact). In spaces, $\pi_0$ preserves products but need not preserve pullbacks. For the basepoint maps into $BG$, $$ *\times_{BG}*\simeq G, \qquad *\times_{\pi_0 BG}*\simeq *. $$ For nontrivial $G$ the component sets differ.
Proof. The first pullback is the based loop space of $BG$, equivalent to the discrete group $G$. The connected space $BG$ has one component. $\square$
Consequently one cannot recover a space of constrained solutions by computing an ordinary quotient first and then adding unspecified higher structure. Nor does Theorem 4.3 assert that $\tau_{\leq n}\lim H$ equals $\lim\tau_{\leq n}H$ for unrestricted diagrams.
Proposition 7.2 (A sufficient exactness condition). Suppose $C,D$ have finite limits, $X:C\to\mathcal S$ preserves products, and $(\int_C X)^{\mathrm{op}}$ is filtered. Then $\operatorname{Lan}_F X$ preserves finite limits for every $F:C\to D$.
Proof. In (1), representables preserve finite limits, and filtered colimits of spaces commute with finite limits [3, Section 5.3.3]. $\square$
Corollary 7.3 (Finite-limit refinement). If $C,D$ have finite limits and $F:C\to D$ preserves them, its comprehensive factorization consists of finite-limit-preserving functors between finitely complete $\infty$-categories.
Proof. For $X=1_C$, its elements category is $C$. The opposite $C^{\mathrm{op}}$ has finite colimits, so every finite diagram has a cocone and $C^{\mathrm{op}}$ is filtered. Proposition 7.2 makes $Y_F$ left exact. For a finite diagram in $\int_DY_F$, its underlying diagram in $D$ has a limit $d$; the compatible elements specify a point in $\lim Y_F(d_i)\simeq Y_F(d)$. The mapping-space fiber calculation of Lemma 2.1 proves that this is a limit upstairs and that the projection reflects limit cones. Consequently $\eta_F$ preserves finite limits because $p_F\eta_F\simeq F$ does. $\square$
The same argument applies to left exact set-valued functors on ordinary finitely complete categories, using ordinary filtered colimits. This sharpens the finite-limit direction raised in [1]: the additional filteredness argument supplies the exactness missing from finite-product hypotheses alone. It does not extend left exactness to arbitrary product-preserving functors or supply a presentation calculus for dependent syntax. Flatness is the relevant general language when the domain lacks the requisite limits.
8. Verification, scope, and further work
The attached Python checks verify finite diamond homology, the degree-one normalized bar homology of a cyclic group, and every lens-law instance in a three-state countermodel. All assertions pass. They check examples, not the general theorems. A practical implementation should retain rewrite witnesses and coherence boundaries and declare its observational level. No complete saturation engine, decidability result, or complexity bound is claimed.
Authorship and automation. Submitted anonymously at the responsible researcher's direction. An AI assistant assisted with literature retrieval, formulation, proofs, source preparation, and finite-example checks. No independent referee review or proof-assistant certification is claimed. Publication and review classification are editorial decisions.
References
1. E. Patterson. *How to prove equations using diagrams, Part 3* (2026). Topos Institute. 2. F. Borceux and B. J. Day. *On product-preserving Kan extensions* (1977). DOI. 3. J. Lurie. *Higher Topos Theory* (2009), Sections 4.1, 5.3.3, 5.5.8, Chapter 6. Text. 4. J. Lurie. *Kerodon*, cofinality. 02N0. 5. J. Lurie. *Kerodon*, siftedness. 02QD. 6. J. Ruit. *Formal category theory in infinity-equipments II* (2024), Section 7.4. arXiv. 7. R. Street and R. F. C. Walters. *The comprehensive factorization of a functor* (1973). DOI. 8. Y. Guiraud and P. Malbos. *Polygraphs of finite derivation type* (2018). arXiv. 9. E. Riehl and D. Verity. *Kan extensions and the calculus of modules for infinity-categories* (2017). arXiv. 10. A. Tiurin, C. Barrett, D. R. Ghica, N. Hu. *Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs* (2025 revision). arXiv. 11. A. Tiurin, D. R. Ghica, N. Hu. *Categorical E-Graphs for Lambda Calculi* (2026 revision). arXiv. 12. The Univalent Foundations Program. *Homotopy Type Theory* (2013). Book.