Scope and main result
Patterson’s initial-functor calculus interprets a sound diagram rewrite as restriction along a functor that preserves cones. This manuscript extends that criterion to homotopy-coherent solutions and tracks exactly which levels of witness data a rewrite preserves. The attached 50-page manuscript gives the proofs, 45 numbered figures, and the bibliography.
For a small shape map $u:A\to K$, let $A_{/k}=A\times_K K_{/k}$, where $K_{/k}\to K$ selects the domain of an arrow to $k$. Define the covariant weight $$ W_{u,n}(k)=\tau_{\le n}|A_{/k}|,\qquad -1\le n\le\infty, $$ where $|{-}|$ is groupoid completion and $\tau_{\le\infty}$ is the identity. The functor $u$ is $n$-initial precisely when $W_{u,n}$ is terminal. This condition is equivalent to the canonical restriction $\lim_K F\to\lim_A Fu$ being an equivalence for every $n$-truncated space-valued diagram on $K$. More generally it is equivalent to preservation of cones in every category with $n$-truncated mapping spaces. If either limit exists in such a category, the other exists and the comparison is an equivalence.
The proof represents the solution functor on space-valued models by the covariant weight $W_u=\operatorname{Lan}_u1_A$. The pointwise Kan extension is the comma-space formula, and for truncated models the representation factors through $\tau_{\le n}W_u$. The Yoneda lemma detects the augmentation by testing all such models. For arbitrary targets one applies the same criterion to the functors of probes.
Factorization, cartesian theories, and parameters
The class of $n$-initial maps is left orthogonal to left fibrations with $n$-truncated fibers. The factorization is $$ A\longrightarrow \int_K W_{u,n}\longrightarrow K. $$ At an object $(k,w)$ of the middle category, the groupoid completion of the comma category for the first map is the homotopy fiber of $W_u(k)\to W_{u,n}(k)$ at $w$. This identifies the first map as $n$-initial. The lifting property is the extension of sections of the corresponding truncated left fibration. At level $0$ for ordinary categories the formula recovers the initial and discrete-opfibration comprehensive factorization.
For finite-product shapes and a product-preserving map, this factorization preserves finite products. The projection from the comma category at $x\times y$ to the product of the comma categories at $x$ and $y$ has a right adjoint obtained by pairing maps out of $u(a\times b)$. Finality of that right adjoint computes the product comparison for the pointwise Kan extension. The same weight then represents solutions on the full subcategory of product-preserving models. Equivalence of truncated weights, natural equivalence of solution functors, and existence of an $n$-initial zigzag over the common theory are equivalent. The zigzag factors through the two associated left fibrations. For a specified comparison over a fixed theory, it suffices that the induced map of relative weights be an equivalence.
The relative criterion in slices of an infinity-topos uses $\tau_{\le n}^B\operatorname{Lan}_u1_B$. Its formation commutes with parameter pullback and geometric inverse image. Effective-epimorphism descent computes global solution spaces by the totalization of local solutions. For ordinary finitary algebras in a Grothendieck topos, the least congruence containing a family of seed pairs is the increasing union of finite closure stages. Each step uses products, pullbacks, images, and unions. The effective quotient therefore commutes with geometric inverse image, as does the corresponding presented free term monad.
Worked calculations and scope
- The source article’s pasting and two-period congruence calculations are recovered by local shape attachments and folds.
- In smooth manifolds, a transverse diagonal inverse image represents its equation. The equalizer of $(x,y)\mapsto xy$ and the zero map has no representing manifold. The two axis probes would force a putative representing map to be submersive at the origin. The smooth solution sheaf exists and includes plots switching axes through flat functions.
- A coherent pullback of one-object groupoids is the action groupoid of isomorphism witnesses. The two double cosets for a subgroup of order two in $S_3$ give $BC_2\amalg *$. Output merging can preserve all set-valued models of a cartesian theory while changing its groupoid solutions.
- A square-root torsor on the circle is locally inhabited and has no global section. A sheaf of automorphisms of an $S_3$-torsor has six witnesses locally and two globally because of conjugation by its monodromy. Lifting the nontrivial $C_2$-torsor on $\mathbb{RP}^2$ through $C_4\to C_2$ gives a nonzero Čech obstruction.
- The free commutative analytic monad on spaces keeps permutation stabilizers that the ordinary multiset monad identifies at the component level. A coherent algebraic relation attachment classifies a map equipped with a chosen path. Attaching a self-relation to a free generator can contribute a circle even when its ordinary congruence is unchanged.
- The full coherent factorization preserves finite-limit contexts under the given hypotheses. At each finite level, the pullback of two points over $K(C_2,n+1)$ gives a counterexample to preservation by the truncated projection.
The result classifies semantic equivalence of diagrams at the chosen level. The finite certificates in the worked examples establish their specific comparisons. The general completeness theorem uses the comprehensively factored shapes, which can be infinite.
Relation to prior work
The ordinary unary and cartesian cases are developed in Evan Patterson’s first article and his subsequent preprint. The article builds on Street and Walters’ comprehensive factorization, higher cofinality and straightening, and the higher cartesian extension considered in the journal’s earlier note. The analytic examples use the free-algebra formulas and the comparison of analytic monads and infinity-operads due to Gepner, Haugseng, and Kock.
Authorship and evidence
The manuscript uses an anonymous byline. The submitting author is responsible for the claims, proofs, and references. An AI assistant assisted with literature retrieval, proof development, manuscript preparation, and diagram typesetting. The evidence consists of the mathematical proofs, worked calculations, and foundational references in the attached paper.