1 Introduction↩︎

Reverse-mode automatic differentiation (AD) transforms a program into one that propagates cotangents backward through its computation. Its efficiency for maps with many inputs and few outputs makes it the standard basis of gradient computation [1]–[3]. A language-level account must make this propagation compositional in substitution, binding, and the source type formers while proving that the transformed program computes the transposed derivative.

Combinatory Homomorphic Automatic Differentiation (CHAD) obtains the transformation from semantics [4]–[6]. Types and programs form a syntactic category, substitution is composition, and the universal property of the syntax extends chosen primal maps and codifferentials to a structure-preserving interpretation. Composition gives the reverse chain rule; products and exponentials generate the corresponding program clauses.

A concrete simply typed model for products and functions is \(\mathsf{Copow}(\mathbf{Vect}^{\mathrm{op}})\). Its objects \((A,V)\) consist of a set of primal values and one cotangent space, and an arrow \((f,f^*):(A,V)\to(B,W)\) has \(f:A\to B\) and \(f_a^*:W\to V\), with \((gf)^*_a=f_a^*g^*_{f(a)}\). The category is cartesian closed. Variants expose its limitation: at a value of \(A+B\), the valid cotangent is the left or right fibre according to the active branch, and \(\mathsf{Copow}(\mathbf{Vect}^{\mathrm{op}})\) does not generally have coproducts. Expressive CHAD therefore uses \(\mathsf{Fam}(\mathbf{Vect}^{\mathrm{op}})\), whose fibres vary with the primal value  [6]; Paszke and Plotkin use the analogous dependent linear representation for sum types [7]. Executable CHAD uses common carriers  [6], while Efficient CHAD develops sparse representations [8]. This leaves open why the simply typed representation presents the dependent semantics and what determines its behaviour outside the valid fibres.

The key observation is that cotangent spaces \(V\) and \(W\) can be represented in \(V\oplus W\) by the projectors \[p_{\mathsf{inl}(a)}(v,w)=(v,0), \qquad p_{\mathsf{inr}(b)}(v,w)=(0,w).\] The dependency is retained as a primal-indexed family of idempotents. Since the Karoubi envelope is the universal category in which idempotents split  [9]–[11], this suggests \[\mathsf{Fam}(\mathbf{Vect}^{\mathrm{op}}) \simeq \mathsf{Kar}\bigl(\mathsf{Copow}(\mathbf{Vect}^{\mathrm{op}})\bigr) \rightsquigarrow \mathsf{Copow}(\mathbf{Vect}^{\mathrm{op}}).\] The equivalence turns projector images into explicit fibres; the semifunctorial passage retains the ordinary carriers and maps but no longer treats their projectors as identities.

We first prove that common retract hosts generate \(\kappa\)-small coproducts in \(\mathsf{Kar}(\mathsf{Copow}_\kappa(\mathcal{C}))\) and characterize when the constant-family inclusion extends to \(\mathsf{Kar}(\mathsf{Copow}_\kappa(\mathcal{C}))\simeq\mathsf{Fam}_\kappa(\mathcal{C})\): precisely when \(\mathcal{C}\) is Cauchy complete and every \(\kappa\)-small family has a common retract host. For \(\mathbf{Vect}^{\mathrm{op}}\), direct sums provide such hosts. We then reproduce the completion inside the ordinary CHAD target. For the freely generated bicartesian closed syntax \(\mathsf{Syn}_{+}\) and ordinary reverse target \(\mathsf T_{\mathsf{Tar}}^{\leftarrow}=\Sigma_{\mathsf C_{\mathsf{Tar}}}\mathsf L_{\mathsf{Tar}}^{\mathrm{op}}\), retaining the generated idempotents gives \[\overleftarrow{\mathcal{D}}_{\mathrm{Kar}}:\mathsf{Syn}_{+}\longrightarrow\mathsf{Kar}(\mathsf T_{\mathsf{Tar}}^{\leftarrow}).\] Its representatives are ordinary nondependent types and terms. At data types the idempotent is \((1,p_\tau)\); at function types cartesian closure projects the entire function–backpropagator package by \(h\mapsto e_\sigma h e_\tau\). Forgetting the distinguished identities gives a composition-preserving semifunctor \(\overleftarrow{\mathcal{D}}_{\mathrm{st}}:\mathsf{Syn}_{+}\rightsquigarrow\mathsf T_{\mathsf{Tar}}^{\leftarrow}\).

Realization by splitting idempotents is naturally isomorphic to dependent CHAD. For a term \(t:\tau\to\sigma\) between the data types of our language, the unique projector-compatible ambient backpropagator is \[\widehat R_t(x)=\iota_{\tau,x}Df(x)^{\mathsf T}\rho_{\sigma,f(x)}.\]

1.0.0.1 Contributions.

1. We construct coproducts of completed constant families from common retract hosts and prove the criterion \(\mathsf{Kar}(\mathsf{Copow}_\kappa(\mathcal{C}))\simeq\mathsf{Fam}_\kappa(\mathcal{C})\).

2. We derive reverse AD with variants as a bicartesian closed interpretation into the completed ordinary target, including explicit variant structure and the higher-order idempotent forced by cartesian closure.

3. We prove equivalence with dependent CHAD, identify ordinary erasure as a semifunctor, and derive the unique ambient correctness formula. The forward dual is given in the appendix.

2 isolates the obstruction, 3 proves the completion theorem, 4 constructs the simply typed interpretation, and 5 proves correctness. The appendices contain all expanded constructions and proofs.

2 Semantics-driven reverse AD and the variant obstruction↩︎

We begin by recalling the universal formulation of CHAD and the two fibrewise-dual target constructions. This separates the general semantics-driven principle from the specific obstruction introduced by variants: reverse differentiation itself remains compositional, but the constant-cotangent target lacks the coproducts needed to interpret branch-dependent fibres.

2.1 Universal source semantics and fibrewise-dual targets↩︎

Let \(\mathsf{Syn}\) be the cartesian-closed syntactic category freely generated by ground types \(\mathsf{real}^n\) and primitive operations, modulo the \(\beta\eta\)-equations and any declared equations among the primitives. Its universal property is the standard categorical semantics of the simply typed lambda calculus [12], [13]: an interpretation of the generators satisfying those equations extends uniquely to a cartesian-closed functor.

Throughout, a bicartesian closed functor means a functor equipped with coherent comparison isomorphisms for the chosen initial object, terminal object, binary products, binary coproducts, and exponentials. When the source is the freely generated syntax and choices have been fixed, we suppress these comparisons from the notation. No strictness assertion is intended.

The target language is organised by a cartesian category \(\mathsf C_{\mathsf{Tar}}\) of primal types and terms and an indexed category \(\mathsf L_{\mathsf{Tar}}:\mathsf C_{\mathsf{Tar}}^{\mathrm{op}}\longrightarrow\mathbf{Cat}\) of linear types and linear terms. Forward and reverse CHAD use the two fibrewise-dual Grothendieck constructions \[\mathsf T_{\mathsf{Tar}}^{\rightarrow}=\Sigma_{\mathsf C_{\mathsf{Tar}}}\mathsf L_{\mathsf{Tar}}, \qquad \mathsf T_{\mathsf{Tar}}^{\leftarrow}=\Sigma_{\mathsf C_{\mathsf{Tar}}}\mathsf L_{\mathsf{Tar}}^{\mathrm{op}}.\] An arrow \((f,f^*):(A,V)\to(B,W)\) of \(\mathsf T_{\mathsf{Tar}}^{\leftarrow}\) consists of a primal term \(f:A\to B\) and a term \(f^*:A;W\to V\) linear in \(W\); composition is substitution in the primal component and reverse accumulation in the linear component. We import the target hypotheses from basic CHAD: \((\mathsf C_{\mathsf{Tar}},\mathsf L_{\mathsf{Tar}})\) is a categorical model of its target language in the sense of [5]. In particular, the forward and reverse total categories are cartesian closed by [5]. Broader closure criteria are given in [14].

Assigning each primitive operation its primal map and derivative therefore induces a forward functor \(\overrightarrow{\mathcal{D}}:\mathsf{Syn}\to\mathsf T_{\mathsf{Tar}}^{\rightarrow}\), while assigning its primal map and codifferential induces the reverse functor \[\overleftarrow{\mathcal{D}}:\mathsf{Syn}\longrightarrow\mathsf T_{\mathsf{Tar}}^{\leftarrow}.\] The two are fibrewise dual. We develop the reverse target below; every completion argument has the forward analogue obtained by removing the fibrewise opposite.

In the source language considered here, a data type is generated from \(\mathsf{real}^n\), \(1\), and \(0\) by finite products and variants. This is the tuple-and-variant data-type fragment of expressive CHAD. The correctness theorem in 5 is stated for source terms whose domain and codomain are data types of this fragment.

This universal account works without variants because the constant-cotangent target has the cartesian closed structure required by products and functions. Coproducts are different: their tangent or cotangent fibre depends on the branch selected by the primal computation. We now make this obstruction precise in the reverse concrete model.

2.2 The coproduct obstruction for constant cotangents↩︎

The concrete constant-cotangent model is \(\mathsf{Copow}(\mathbf{Vect}^{\mathrm{op}})\). Its terminal object and binary products are \[1=(1,0), \qquad (A,V)\times(B,W)=(A\times B,V\oplus W).\]

The obstruction created by variants is now concrete.

In \(\mathsf{Fam}(\mathbf{Vect}^{\mathrm{op}})\) the corresponding coproduct is branchwise: \[(A,V_{(-)})+(B,W_{(-)})=(A+B,Z_{(-)}),\] where \(Z_{\mathsf{inl}(a)}=V_a\) and \(Z_{\mathsf{inr}(b)}=W_b\). This is the cotangent semantics of variants in expressive CHAD [6].

The obstruction is therefore not a failure of differentiation, but a mismatch between two free completions: basic CHAD admits only constant families, whereas variants require arbitrary families. The next section shows how common ambient hosts create the missing coproducts and when the resulting completion agrees with the family semantics.

3 Coproducts and Cauchy completion of constant families↩︎

The preceding obstruction compares two semantic universes. Constant families suffice for basic nondependent CHAD, while variants require fibres that vary with the selected primal branch. We now show that a common ambient object already supplies the missing coproducts after idempotents are split. Cauchy completeness then determines when this completed constant-family category agrees with the full family category.

Fix a regular infinite cardinal \(\kappa\). A set is \(\kappa\)-small when its cardinality is less than \(\kappa\). For the unadorned constructions used in the higher-order semantics, we fix Grothendieck universes \(\mathcal{U}\in\mathcal{V}\): sets, families, and vector spaces are \(\mathcal{U}\)-small, and the resulting categories are regarded as \(\mathcal{V}\)-categories. Appendix 9 records the size conventions in full.

3.1 Free coproduct, copower, and Cauchy completions↩︎

For a category \(\mathcal{C}\), the category \(\mathsf{Fam}_\kappa(\mathcal{C})\) has \(\kappa\)-small families \((X_i)_{i\in I}\) as objects. A morphism \[(u,\alpha):(X_i)_{i\in I}\longrightarrow(Y_j)_{j\in J}\] consists of a function \(u:I\to J\) and arrows \(\alpha_i:X_i\to Y_{u(i)}\). The singleton-family embedding \[\eta_{\mathcal{C}}:\mathcal{C}\longrightarrow\mathsf{Fam}_\kappa(\mathcal{C})\] exhibits \(\mathsf{Fam}_\kappa(\mathcal{C})\) as the free completion of \(\mathcal{C}\) under \(\kappa\)-small coproducts [10], [15].

The full subcategory on constant families is \(\mathsf{Copow}_\kappa(\mathcal{C})\). Its objects are pairs \((I,X)\), and it is the free completion of \(\mathcal{C}\) under copowers by \(\kappa\)-small sets. We write \[\iota_{\mathcal{C}}:\mathcal{C}\longrightarrow\mathsf{Copow}_\kappa(\mathcal{C})\] for the singleton embedding and \[J_{\mathcal{C}}:\mathsf{Copow}_\kappa(\mathcal{C})\hookrightarrow\mathsf{Fam}_\kappa(\mathcal{C})\] for the constant-family inclusion.

The Karoubi envelope \(\mathsf{Kar}(\mathcal{A})\) has objects \((A,e)\), where \(e:A\to A\) is idempotent, and arrows \(f:(A,e)\to(B,d)\) satisfying \(f=dfe\). Its identity on \((A,e)\) is \(e\). The canonical embedding \(Q_{\mathcal{A}}:\mathcal{A}\to\mathsf{Kar}(\mathcal{A})\) is the free Cauchy completion: for every Cauchy-complete category \(\mathcal{D}\), restriction induces an equivalence \[[\mathsf{Kar}(\mathcal{A}),\mathcal{D}] \simeq [\mathcal{A},\mathcal{D}].\] See [9]–[11]; the universal properties and our variance conventions are recalled in the appendices.

The three constructions now have distinct roles. The copower completion provides the constant ambient carriers available to nondependent CHAD. The Karoubi envelope separates the subobjects selected by idempotents on those carriers. The family completion presents the resulting fibres directly. We first show that the common-host hypothesis already equips the Karoubi-completed constant-family category with the required coproducts.

3.2 Coproducts in the Karoubi-completed constant-family category↩︎

A common retract host allows several ambient objects to be represented inside a single carrier. We first isolate this change of carrier.

Once all objects have the same ambient carrier, their coproduct is obtained by concatenating the index sets and assembling the idempotents blockwise.

The common-host hypothesis is used only to replace the ambient objects \(X_a\) by a single carrier \(P\). Once this has been done, the coproduct is formed by concatenating the index sets and assembling the corresponding idempotents blockwise.

A component-by-component verification, including the empty coproduct, is given in [app:common-carrier-details,app:coproduct-details].

A useful sufficient condition is the existence of zero morphisms together with the relevant products or coproducts. Indeed, if \(\mathcal{C}\) has zero morphisms and \(\kappa\)-small coproducts, then the coproduct of any \(\kappa\)-small family is a common retract host: the coproduct injection serves as the section, while the retraction is the morphism that is the identity on the selected summand and zero on every other summand. More generally, we have the following result.

3.3 Cauchy density and the family-completion equivalence↩︎

The preceding proposition supplies the colimit structure required by variants. To identify the resulting category with \(\mathsf{Fam}_\kappa(\mathcal{C})\), one further condition is needed:

A fully faithful functor \(J:\mathcal{A}\to\mathcal{B}\) is Cauchy dense when every object of \(\mathcal{B}\) is a retract of an object in the image of \(J\). By 4:

This observation links the explicit coproducts of [prop:kar-coprod] with the universal comparison between the two completions.

Under this equivalence, a family \((V_i)_{i\in I}\) is represented by the ambient space \(\bigoplus_iV_i\) together with the coordinate projectors \(\iota_i\pi_i\). Conversely, splitting these projectors recovers the original fibres. One could instead use direct-product ambient spaces; the two choices give isomorphic coproduct objects after completion, although their ambient presentations differ. We use direct sums because they provide the sparse, finitely supported presentation relevant to reverse-mode implementations.

4 A structure-preserving simply typed transformation↩︎

The completion theorem identifies the correct semantic target. We next lift that result from concrete families of vector spaces to the syntactic target language of CHAD. The construction proceeds in two stages: first we recover the missing bicartesian structure inside the Karoubi envelope; then the universal property of the source syntax generates the transformation.

4.1 Variant coproducts in the completed target↩︎

We use the ordinary reverse target \(\mathsf T_{\mathsf{Tar}}^{\leftarrow}\) of basic CHAD.

4.1.0.1 Variant-target assumption.

We assume that \((\mathsf C_{\mathsf{Tar}},\mathsf L_{\mathsf{Tar}})\) is a categorical model of the basic CHAD target language in the sense of [5]. Thus \(\mathsf L_{\mathsf{Tar}}\) is locally indexed, its fibres have the finite-biproduct and cartesian linear-function structure required by CHAD, and \(\mathsf T_{\mathsf{Tar}}^{\leftarrow}\) is cartesian closed by [5]. For variants, the only additional assumption is that \(\mathsf C_{\mathsf{Tar}}\) has finite coproducts.

The remaining operations needed below are consequences of these hypotheses. Finite biproducts in the fibres provide common retract hosts in the reverse fibres. Moreover, cartesian linear-function objects and the coproduct universal property in \(\mathsf C_{\mathsf{Tar}}\) give natural bijections \[\mathsf L_{\mathsf{Tar}}(A+B)(U,P) \cong \mathsf L_{\mathsf{Tar}}(A)(U,P)\times\mathsf L_{\mathsf{Tar}}(B)(U,P),\] so linear maps over \(A+B\) are uniquely determined by their two branch restrictions. The associated branchwise linear case operation, including its \(\beta\)- and \(\eta\)-equations and stability under reindexing, is therefore derived rather than assumed. Appendix 15 gives the full argument.

The following calculations are written in the internal language of \(\mathsf C_{\mathsf{Tar}}\) and its indexed linear calculus. Equivalently, each displayed elementwise equation denotes the corresponding equality of target terms. We call an idempotent \(e=(r,p)\) on a reverse-target object full when it acts on the whole primal/function–backpropagator package, rather than only on a cotangent coordinate.

Let \[E=((A,V),e), \qquad F=((B,W),d),\] where \(e=(r,p)\) and \(d=(s,q)\) are idempotent endomorphisms in \(\mathsf T_{\mathsf{Tar}}^{\leftarrow}\). On the ambient object \((A+B,V\oplus W)\), define \(c_{E,F}\) by \[\begin{align} c_{E,F,1}(\mathsf{inl}(a))&=\mathsf{inl}(r(a)), & (c_{E,F})^*_{\mathsf{inl}(a)}(v,w)&=(p_a(v),0),\\ c_{E,F,1}(\mathsf{inr}(b))&=\mathsf{inr}(s(b)), & (c_{E,F})^*_{\mathsf{inr}(b)}(v,w)&=(0,q_b(w)). \end{align}\] For an idempotent in the reverse target, the backward equations are \(p_a\circ p_{r(a)}=p_a\) and \(q_b\circ q_{s(b)}=q_b\). Hence \(c_{E,F}^2=c_{E,F}\) branchwise. Define \[E+F:=((A+B,V\oplus W),c_{E,F}).\] This is the coproduct object in the completed category; no dependent target type former is required.

Under 1, this coproduct realizes to the branchwise coproduct in \(\mathsf{Fam}(\mathbf{Vect}^{\mathrm{op}})\). It is therefore an ambient presentation of the established dependent variant semantics, not a competing interpretation.

Having reconstructed the missing coproducts in the completed target, the rest of the transformation follows from the source universal property. This is the decisive methodological point: the clauses for variants are not appended to CHAD by hand, but are forced by the same preservation principle as the clauses for products and functions.

4.2 The universal completed interpretation↩︎

Let \(\mathsf{Syn}_{+}\) be the bicartesian closed syntactic category freely generated by the source ground types and primitive operations, modulo the declared equations. Products, variants, and function types are supplied by its chosen bicartesian closed structure.

Concretely, for every source type \(\tau\) write \[\overleftarrow{\mathcal{D}}_{\mathrm{Kar}}(\tau) = \bigl((\widehat D_1\tau,\widehat D_2\tau),e_\tau\bigr), \qquad e_\tau=(r_\tau,p_\tau),\] where \(e_\tau\) is a full idempotent endomorphism of the ordinary reverse target object. For data types, induction gives \(r_\tau=1\) and the linear component \(p_\tau(x,-)\) is an idempotent cotangent projector. At ground types it is the identity. Products and sums act componentwise; in particular, \[\begin{align} \widehat D_1(\tau+\sigma) &=\widehat D_1\tau+\widehat D_1\sigma,\\ \widehat D_2(\tau+\sigma) &=\widehat D_2\tau\oplus\widehat D_2\sigma,\\ p_{\tau+\sigma}(\mathsf{inl}(x),(v,w)) &=(p_\tau(x,v),0),\\ p_{\tau+\sigma}(\mathsf{inr}(y),(v,w)) &=(0,p_\sigma(y,w)). \end{align}\] At a function type, however, \[e_{\tau\Rightarrow\sigma} = \varepsilon_{e_\tau,e_\sigma},\] the exponential idempotent induced by cartesian closure. Internally it sends an ambient function–backpropagator package \(h\) to \(e_\sigma h e_\tau\); its primal component need not be the identity. The idempotents are generated code, not proof objects. A transformed term is an ordinary primal computation and backpropagator satisfying the full sandwich equation at its source and target. Appendix 14 gives the concrete exponential idempotent explicitly.

The coproduct object, injections, and copairing above determine all four variant constructs—left and right injection, abort, and case analysis—without an ad hoc semantic clause. Appendix 16 gives the resulting injection and case-analysis terms in full. Product and higher-order clauses are those generated by basic CHAD, restricted by the source and target idempotents; we do not duplicate its full macro here.

The fibrewise-dual forward construction and its ambient formula are recorded in Appendix 18.

The Karoubi-valued functor is the primary semantic construction. The ordinary nondependent program is obtained only after a deliberate change of viewpoint in which the ambient carriers and maps are retained but their distinguished idempotents are no longer treated as categorical identities.

4.3 Idempotent erasure and semifunctoriality↩︎

A semifunctor preserves objects, arrows, and composition, but need not preserve identities. Hoofman and Moerdijk showed, building on Hayashi and Hoofman, that the theory of semifunctors embeds fully into ordinary functor theory through Karoubi completion [16]–[18]. Forgetting the distinguished status of the idempotent attached to each Karoubi object gives such a map \[\overleftarrow{\mathcal{D}}_{\mathrm{st}}:\mathsf{Syn}_{+}\rightsquigarrow\mathsf T_{\mathsf{Tar}}^{\leftarrow}.\]

Equivalently, every semifunctor \(F:\mathcal{X}\rightsquigarrow\mathcal{A}\) determines an ordinary functor \(\mathcal{X}\to\mathsf{Kar}(\mathcal{A})\) by sending \(X\) to \((FX,F1_X)\). This is the concrete form, used here, of the Hoofman–Moerdijk passage from semifunctors to ordinary functors; the appendices prove the correspondence explicitly. Notice that this forgetful passage does not remove projector calls required by the generated program. It forgets only their distinguished categorical role as identities of completed objects.

Structure preservation explains how the algorithm is generated, but it does not by itself identify the linear map computed on the entire ambient carrier. The next section compares the completed semantics with dependent CHAD and derives the exact extension of the mathematical derivative to invalid ambient coordinates.

5 Correctness of the ambient simply typed realization↩︎

We now compare the completed target with the concrete dependent model and use the Karoubi equations to determine the ambient backpropagator.

5.1 Concrete realization and comparison↩︎

5.1.0.1 Concrete-model assumption.

Assume a primal interpretation \(\mathcal{S}:\mathsf C_{\mathsf{Tar}}\to\mathbf{Set}\) and compatible indexed linear interpretations \(\mathcal{L}_A:\mathsf L_{\mathsf{Tar}}(A)\to\mathbf{Vect}^{\mathcal{S} A}\). A linear object \(V\) is sent to the constant family at a vector space \(\mathcal{V} V\), and reindexing is interpreted by substitution. Assume the usual basic-CHAD comparison maps, so the induced reverse-total interpretation preserves the chosen terminal object, products, and exponentials, and assume additionally that finite coproducts, zero objects, biproducts, and linear-function objects are preserved. In particular, \[\begin{align} \mathcal{S}(A+B)&\cong\mathcal{S} A+\mathcal{S} B,\\ \mathcal{V}(V\oplus W)&\cong\mathcal{V} V\oplus\mathcal{V} W,\\ \mathcal{S}(V\multimap W)&\cong\mathbf{Vect}(\mathcal{V} V,\mathcal{V} W). \end{align}\] Ground types have their usual Euclidean interpretations, and primitives use the same primal maps and codifferentials as dependent CHAD. These data induce \[\llbracket-\rrbracket_\mathsf{Tar}:\mathsf T_{\mathsf{Tar}}^{\leftarrow}\longrightarrow\mathsf{Copow}(\mathbf{Vect}^{\mathrm{op}}), \qquad \llbracket(A,V)\rrbracket_\mathsf{Tar}=(\mathcal{S} A,\mathcal{V} V),\] with \(\llbracket(f,\ell)\rrbracket_\mathsf{Tar}= (\mathcal{S} f,(\mathcal{L}_A(\ell)_a)_{a\in\mathcal{S} A})\). Karoubi completion followed by realization gives \[\llbracket-\rrbracket_{\mathrm{cpl}}: \mathsf{Kar}(\mathsf T_{\mathsf{Tar}}^{\leftarrow}) \xrightarrow{\mathsf{Kar}(\llbracket-\rrbracket_\mathsf{Tar})} \mathsf{Kar}(\mathsf{Copow}(\mathbf{Vect}^{\mathrm{op}})) \xrightarrow{\mathfrak R} \mathsf{Fam}(\mathbf{Vect}^{\mathrm{op}}).\]

Let \(\overleftarrow{\mathcal{D}}_{\mathrm{dep}}:\mathsf{Syn}_{+}\to\mathsf{Fam}(\mathbf{Vect}^{\mathrm{op}})\) denote the standard dependent reverse-CHAD interpretation.

Every data type generated from \(\mathsf{real}^n\), \(1\), and \(0\) by finite products and variants is isomorphic, by repeated distributivity, to a finite sum of finite products of Euclidean ground types. The tuple-and-variant correctness theorem of expressive CHAD therefore applies componentwise  [6], and correctness transports along these canonical structural isomorphisms.

5.2 Projector-compatible ambient correctness↩︎

For a data type \(\tau\) and value \(x\), let \(T^*_\tau(x)\) be the genuine cotangent fibre and \(\widehat T^*_\tau\) its ambient cotangent space. Fix the splitting \[T^*_\tau(x) \xrightarrow{\iota_{\tau,x}} \widehat T^*_\tau \xrightarrow{\rho_{\tau,x}} T^*_\tau(x), \qquad \rho_{\tau,x}\iota_{\tau,x}=1, \quad \iota_{\tau,x}\rho_{\tau,x}=p_{\tau,x}.\] An ambient extension \(h\) of \(k:T^*_\sigma(f(x))\to T^*_\tau(x)\) is projector compatible when \(h=p_{\tau,x}hp_{\sigma,f(x)}\) and \(\rho_{\tau,x}h\iota_{\sigma,f(x)}=k\).

In particular, \(\widehat R_{1_\tau}(x)=p_{\tau,x}\), while adjacent retraction–section pairs cancel under composition.

6 Related work and scope↩︎

Basic and expressive CHAD provide, respectively, the higher-order semantics-driven transformation and the dependent-family correctness result used here [4]–[6]. Efficient and iterative CHAD study sparse accumulation and partial or iterative computation  [8], [19], [20]. For sums, Paszke and Plotkin likewise use dependent linear types selected by the active branch [7]. Our contribution is the denotational equivalence between such fibres and ordinary ambient types with idempotents, including the reconstructed bicartesian closed structure and the uniquely compatible ambient derivative; it is not a new asymptotic AD algorithm.

Other compositional accounts use lenses, reverse derivative categories, continuations, control, or linear negation  [21]–[27]. Karoubi completion and semifunctors also occur in denotational and quantum semantics [16]–[18], [28], [29]. Our correctness theorem concerns exactly finite products and variants of Euclidean ground types.

7 Conclusion↩︎

Idempotent completion turns ambient simply typed cotangents into a bicartesian closed model of variants equivalent to the dependent family semantics. Realization recovers dependent CHAD, erasure yields its ordinary semifunctorial program, and the sandwich equations force the unique ambient derivative extension. The forward dual is given in the appendix.

7.0.0.1 Funding.

This research was supported by the ERC project FoRECAST. The first author was also supported by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) through the project Higher-Order Monad-based Programming and Reasoning (HOMBRe), project number 501369690, led by Sergey Goncharov, during his postdoctoral appointment at the School of Computer Science, University of Birmingham. He was further supported by the Fields Institute for Research in Mathematical Sciences through a Fields Research Fellowship in 2023, and by the Centre for Mathematics of the University of Coimbra (CMUC) under the Fundação para a Ciência e a Tecnologia (FCT), through the grants UID/00324/2025 and UID/PRR/00324/2025.

7.0.0.2 Data availability.

This work is theoretical and does not use or generate research data.

8 Key ideas: from dependent fibres to simply typed programs↩︎

This appendix gives a conceptual map of the construction for readers coming from programming languages, category theory, or automatic differentiation. It omits most universal-property proofs, which begin in 9, and concentrates on what changes—and what does not—when dependent cotangent fibres are presented by ordinary simply typed carriers.

8.1 The semantic mismatch↩︎

A reverse-mode value has two parts: a primal value and a space in which cotangents for that value live. For a source type without variants, one may use one cotangent space for every primal value. This gives the constant-family model \[\mathsf{Copow}(\mathbf{Vect}^{\mathrm{op}}).\] A variant value is different. At \(\mathsf{inl}(a)\) only a left cotangent is valid, while at \(\mathsf{inr}(b)\) only a right cotangent is valid. The intrinsic semantic object is therefore a family \[x\longmapsto T^*_\tau(x),\] represented in \(\mathsf{Fam}(\mathbf{Vect}^{\mathrm{op}})\). The dependence is essential: it expresses which cotangents are meaningful at the current primal value.

The implementation problem is that a direct internal language for such a family uses a cotangent type depending on the primal term. Ordinary implementations, however, prefer one target type for every source type.

8.2 Keep the dependency as a projector↩︎

Choose one ambient space \(\widehat T^*_\tau\) large enough to contain every fibre \(T^*_\tau(x)\) as a retract. For each primal value \(x\), choose maps \[T^*_\tau(x) \xrightarrow{\iota_{\tau,x}} \widehat T^*_\tau \xrightarrow{\rho_{\tau,x}} T^*_\tau(x), \qquad \rho_{\tau,x}\iota_{\tau,x}=1.\] Their composite \[p_{\tau,x}=\iota_{\tau,x}\rho_{\tau,x}\] is an idempotent on the single ambient type. Its image is the valid cotangent fibre. Thus a dependent family can be presented by two simply typed pieces of data: \[\text{one ambient carrier} \quad+\quad \text{a primal-indexed projector}.\] For a sum, the ambient carrier is a biproduct and the projector selects the active branch: \[\begin{align} p_{\tau+\sigma}(\mathsf{inl}(x),(v,w))&=(p_\tau(x,v),0),\\ p_{\tau+\sigma}(\mathsf{inr}(y),(v,w))&=(0,p_\sigma(y,w)). \end{align}\] Nothing dependent has been approximated or forgotten; its information has moved from the target type into an idempotent target term.

8.3 Why the Cauchy completion is the right category↩︎

The ordinary constant-family category sees the ambient carrier but treats its identity map as the identity. The semantic fibre, however, behaves as if the projector \(p_x\) were the identity: valid values are fixed by \(p_x\), and valid maps satisfy sandwich equations. The Karoubi envelope makes this viewpoint literal. An object is a pair \((A,e)\) with \(e^2=e\), its identity is \(e\), and an arrow \(h:(A,e)\to(B,d)\) satisfies \[h=dhe.\] Consequently, \[\mathsf{Fam}(\mathbf{Vect}^{\mathrm{op}}) \simeq \mathsf{Kar}\bigl(\mathsf{Copow}(\mathbf{Vect}^{\mathrm{op}})\bigr)\] expresses that an explicit family of fibres and an ambient carrier with projectors are two presentations of the same semantic object. The relevant completion is \(\mathsf{Kar}(\mathsf{Copow}(\mathbf{Vect}^{\mathrm{op}}))\), not \(\mathsf{Kar}(\mathsf{Fam}(\mathbf{Vect}^{\mathrm{op}}))\): the latter is already equivalent to \(\mathsf{Fam}(\mathbf{Vect}^{\mathrm{op}})\) because the family category is Cauchy complete.

The general theorem isolates the precise hypotheses. The constant-family inclusion extends along idempotent completion to an equivalence with all \(\kappa\)-small families if and only if \(\mathcal{C}\) is Cauchy complete and every such family has a common retract host. For vector spaces, the host is a direct sum and every idempotent splits through its image.

8.4 One transformation, three views↩︎

The construction has three compatible levels: \[\begin{array}{ccl} \mathsf{Fam}(\mathbf{Vect}^{\mathrm{op}}) &\simeq& \mathsf{Kar}(\mathsf{Copow}(\mathbf{Vect}^{\mathrm{op}})) \quad\rightsquigarrow\quad \mathsf{Copow}(\mathbf{Vect}^{\mathrm{op}})\\[2mm] \text{dependent fibres} && \text{ambient carrier + identities} \qquad \text{ambient carrier only.} \end{array}\] The left presentation is best for stating the mathematical semantics and proving logical-relations correctness. The middle presentation is best for preserving products, variants, and higher-order functions: it is an ordinary category in which the projectors are the identities of the represented fibres. The right presentation is the executable simply typed program obtained by forgetting only that distinguished categorical role. The corresponding idempotent calls remain in the code.

This final passage is a semifunctor rather than a functor. Composition is still strict, because composition in the Karoubi envelope is ambient composition. Identities become the generated idempotents: \[\overleftarrow{\mathcal{D}}_{\mathrm{st}}(1_\tau)=e_\tau.\] At data types, \(e_\tau=(1,p_\tau)\), so the primal identity is unchanged while the cotangent identity discards invalid coordinates.

8.5 Variants and higher-order functions↩︎

For variants, completion creates the missing coproduct. Its ordinary ambient type is \[(A+B,V\oplus W),\] but its identity is the branch-sensitive idempotent. The coproduct injections and case analysis are obtained by sandwiching the ordinary terms with the source and target idempotents. This is why the resulting clauses satisfy the coproduct equations at the completed level even though the ordinary constant-cotangent category lacks coproducts.

At higher-order types, projecting only the cotangent coordinate is insufficient: an ambient function–backpropagator package may itself fail to respect the represented input and output fibres. Cartesian closure generates the required full idempotent. Internally it sends \[h\longmapsto e_\sigma h e_\tau.\] Its fixed points are precisely the projector-compatible function packages. Restricted evaluation and currying then give the higher-order translation. No separate ad hoc rule is needed.

8.6 Why the ambient derivative is forced↩︎

Let \(h:\widehat T^*_\sigma\to\widehat T^*_\tau\) be an ambient backpropagator. Correctness on the genuine fibres requires \[\rho_{\tau,x}h\iota_{\sigma,f(x)}=Df(x)^{\mathsf T},\] while being a completed arrow requires \[h=p_{\tau,x}hp_{\sigma,f(x)}.\] Substituting \(p=\iota\rho\) leaves no freedom: \[h = \iota_{\tau,x}Df(x)^{\mathsf T}\rho_{\sigma,f(x)}.\] The formula explains the whole program: project the incoming ambient cotangent to the valid output fibre, apply the genuine transposed derivative, and embed the result into the ambient input carrier.

It also explains the apparently asymmetric functorial laws. For an identity, \(Df(x)^{\mathsf T}=1\) and hence \(h=p_{\tau,x}\). For a composite, the middle retraction–section pair cancels: \[\rho_{\sigma,f(x)}\iota_{\sigma,f(x)}=1,\] so the ordinary chain rule yields strict preservation of composition.

8.7 Semantics versus representation↩︎

The theorem does not prescribe a dense run-time representation. An ambient direct sum is the semantic vector space in which linear accumulation is defined; an implementation may realise it sparsely, use tagged carriers, or apply the accumulation techniques of Efficient CHAD. The completion result supplies the missing semantic invariant: whatever representation is chosen must implement the projectors and the sandwich equations. In this sense, dependent and simply typed reverse AD are not competing algorithms. They are the same semantics-driven transformation viewed through explicit fibres, completed ambient carriers, and executable ordinary terms.

9 Size conventions and notation↩︎

Fix a regular infinite cardinal \(\kappa\). A set is \(\kappa\)-small when its cardinality is less than \(\kappa\). The subscripted constructions \(\mathsf{Fam}_\kappa\) and \(\mathsf{Copow}_\kappa\) use \(\kappa\)-small index sets; regularity ensures that a \(\kappa\)-small coproduct of \(\kappa\)-small sets is again \(\kappa\)-small. These assumptions are all that the completion theorem requires. For the unadorned higher-order semantic categories \(\mathsf{Fam}\) and \(\mathsf{Copow}\), we fix a Grothendieck universe of small sets large enough to contain the relevant function sets and direct sums. Thus the cartesian-closed constructions below are universe-small without imposing an unsupported closure property on an arbitrary regular infinite cardinal. The finite version is obtained by replacing the \(\kappa\)-small doctrine with finite sets throughout. Our conventions for free completions, enriched copowers, and Cauchy completion follow the standard accounts in [9]–[11].

We write \(\mathbf{Vect}\) for real vector spaces and linear maps, \(\mathbf{Vect}^{\mathrm{op}}\) for its opposite, and \(\mathbf{Set}_{*}\) for pointed sets and basepoint-preserving maps. Our section–retraction notation is always internal to the category under discussion. In particular, in \(\mathbf{Vect}^{\mathrm{op}}\) a section is represented by a projection in \(\mathbf{Vect}\), and a retraction by an inclusion in \(\mathbf{Vect}\). For categories \(\mathcal{A}\) and \(\mathcal{D}\), the functor category is denoted \([\mathcal{A},\mathcal{D}]\).

10 Free completions by families and copowers↩︎

We begin with the two free completions whose difference creates the variant obstruction. Arbitrary families freely add coproducts, while constant families freely add only set-indexed copowers. These constructions are standard instances of free cocompletion [10], [15]; family categories are also the semantic mechanism used for expressive CHAD and arise naturally in familial descent [6], [30]. Making both universal properties explicit fixes the variance and coherence conventions used throughout the later completion argument.

10.1 The free coproduct completion↩︎

If \((X_i^a)_{i\in I_a}\) is a \(\kappa\)-small family of objects of \(\mathsf{Fam}_\kappa(\mathcal{C})\) indexed by \(a\in A\), then its coproduct is concatenation: \[\coprod_{a\in A}(X_i^a)_{i\in I_a} = (X_i^a)_{(a,i)\in\coprod_{a\in A}I_a}.\] The injection from the \(a\)-th summand uses the inclusion \(I_a\to\coprod_b I_b\) and identity component arrows.

The following universal property is the standard free completion by families; see, for example, [10] and [15].

The family construction is the standard free coproduct completion used in the semantics of expressive CHAD [6]; see also the general free-cocompletion accounts in [10], [15] and the use of family categories in familial descent [30].

The constant-family subcategory retains the same morphism calculus but suppresses variation in the fibre object. Its universal property is correspondingly weaker: it freely supplies copowers, rather than arbitrary coproducts.

10.2 The free copower completion↩︎

The singleton embedding is \[\iota_\mathcal{C}:\mathcal{C}\longrightarrow\mathsf{Copow}_\kappa(\mathcal{C}), \qquad X\longmapsto(1,X).\] For a \(\kappa\)-small set \(S\), define \[S\cdot(I,X)=(S\times I,X).\] There is a natural bijection \[\mathsf{Copow}_\kappa(\mathcal{C}) \bigl(S\cdot(I,X),(J,Y)\bigr) \cong \mathbf{Set}\Bigl(S,\mathsf{Copow}_\kappa(\mathcal{C})((I,X),(J,Y))\Bigr),\] obtained by currying the base function \(S\times I\to J\) and the \(S\times I\)-indexed component arrows. Thus \(S\cdot(I,X)\) is the copower by \(S\).

The analogous copower completion is standard enriched-category theory; see [10].

11 Karoubi completion and semifunctors↩︎

The two free completions above add different colimit structure. The Karoubi envelope performs a different operation: it adds the retracts already encoded by idempotents. We use the classical universal description of Cauchy completion [9]–[11] and the semifunctorial perspective developed in programming-language semantics by Hayashi, Hoofman, and Hoofman–Moerdijk [16]–[18]. This is precisely the operation that turns an ambient cotangent carrier with projectors into its family of genuine fibres.

11.1 The Karoubi envelope↩︎

The condition \(f=dfe\) is equivalent to the pair of equations \(f=fe=df\). The canonical embedding is \[Q_\mathcal{A}:\mathcal{A}\longrightarrow\mathsf{Kar}(\mathcal{A}), \qquad A\longmapsto(A,1_A).\] Every \((A,e)\) is a retract of \(Q_\mathcal{A}(A)\): both the section and the retraction are represented by \(e\), and their composite on \((A,e)\) is \(e\), the identity of that Karoubi object.

A category is Cauchy complete, or idempotent complete, when every idempotent splits. For ordinary categories this is equivalent to admitting all absolute colimits [9]–[11].

The following universal property is the classical description of Cauchy completion by splitting idempotents [9]–[11].

11.2 Semifunctors↩︎

A semifunctor \(F:\mathcal{X}\rightsquigarrow\mathcal{A}\) assigns objects and arrows and preserves composition, but is not required to preserve identities [17], [18]. For every object \(X\), put \(e_X=F(1_X)\). Then \[e_X^2=F(1_X1_X)=e_X,\] and for \(f:X\to Y\), \[F(f)=F(1_Yf1_X)=e_YF(f)e_X.\] Thus \(F(f)\) is a Karoubi arrow \((FX,e_X)\to(FY,e_Y)\).

The correspondence below is the object-and-arrow form of the embedding of semifunctor theory into ordinary functor theory developed by Hayashi, Hoofman, and Hoofman–Moerdijk [16]–[18].

Taking as transformations the families \(\theta_X:FX\to GX\) satisfying naturality and \[\theta_X=G1_X\,\theta_X\,F1_X\] yields an equivalence of categories between semifunctors with these transformations and ordinary functors into the Karoubi envelope.

12 Coproducts, Cauchy completion, and ambient representations↩︎

This appendix gives a self-contained proof of the categorical result used in 3. The argument has three steps. First, the common-host condition produces explicit \(\kappa\)-small coproducts in the Karoubi envelope of the constant-family category. Second, the same condition is identified with Cauchy density of the constant-family inclusion. Finally, Cauchy density and idempotent completeness yield the equivalence with the full family category. We conclude by recording the concrete passage between explicit families and ambient carriers equipped with idempotents.

Throughout, \(\kappa\) is a regular infinite cardinal and \(\mathcal{C}\) is a category. The category \(\mathsf{Fam}_\kappa(\mathcal{C})\) has \(\kappa\)-small families \((X_i)_{i\in I}\) as objects. A morphism \[(u,\alpha):(X_i)_{i\in I}\longrightarrow(Y_j)_{j\in J}\] consists of a function \(u:I\to J\) and arrows \(\alpha_i:X_i\to Y_{u(i)}\). The full subcategory on the constant families is \(\mathsf{Copow}_\kappa(\mathcal{C})\); its objects are written \((I,X)\). We denote the constant-family inclusion by \[J_{\mathcal{C}}:\mathsf{Copow}_\kappa(\mathcal{C}) \hookrightarrow\mathsf{Fam}_\kappa(\mathcal{C}).\] An object of \(\mathsf{Kar}(\mathsf{Copow}_\kappa(\mathcal{C}))\) is written \[E=((I,X),(u,p)),\] where \(u^2=u\) and \(p_{u(i)}p_i=p_i\) for every \(i\in I\).

12.1 Coproducts from common retract hosts↩︎

Recall that a family \((X_a)_{a\in A}\) has a common retract host if there are an object \(P\) and arrows \[X_a\xrightarrow{s_a}P\xrightarrow{r_a}X_a, \qquad r_as_a=1_{X_a},\] for every \(a\in A\).

12.2 The blockwise coproduct↩︎

The construction has a simple interpretation. The host condition is used only to place all ambient objects over one carrier \(P\); the coproduct then concatenates the index sets and places the corresponding idempotents on disjoint blocks. Different choices of host may give different ambient representatives, but the resulting coproducts are canonically isomorphic by the universal property.

12.3 Cauchy density and the completion theorem↩︎

We first isolate the standard Cauchy-density argument used below.

Since \(J_{\mathcal{C}}\) is fully faithful, the preceding lemma immediately gives \[J_{\mathcal{C}}\text{ is Cauchy dense} \quad\Longleftrightarrow\quad \text{every \kappa-small family in \mathcal{C} has a common host}.\]

12.3.0.1 Detailed proof of 1.

Assume (2). By 9, \(\mathsf{Fam}_\kappa(\mathcal{C})\) is Cauchy complete. By 10, the fully faithful inclusion \(J_{\mathcal{C}}\) is Cauchy dense. Its extension along \[Q:\mathsf{Copow}_\kappa(\mathcal{C}) \longrightarrow \mathsf{Kar}(\mathsf{Copow}_\kappa(\mathcal{C}))\] therefore exists by the universal property of the Karoubi envelope and is an equivalence by 8. This gives (1). The existence of \(\kappa\)-small coproducts in the source of \(\mathfrak R\) was proved independently in [prop:kar-coprod].

Conversely, assume (1). The category \(\mathsf{Kar}(\mathsf{Copow}_\kappa(\mathcal{C}))\) is Cauchy complete, so its equivalent category \(\mathsf{Fam}_\kappa(\mathcal{C})\) is Cauchy complete. By 9, \(\mathcal{C}\) is Cauchy complete. Moreover, \(Q\) is Cauchy dense and \(\mathfrak RQ\cong J_{\mathcal{C}}\); hence \(J_{\mathcal{C}}\) is Cauchy dense. By 10, every \(\kappa\)-small family has a common retract host.

It remains to identify the chosen coproducts. For \(i\in\operatorname{Fix}(u_a)\), choose a splitting \[X_a\xrightarrow{q^a_i}X^a_i\xrightarrow{m^a_i}X_a\] of \(p^a_i\). The block idempotent \(s_ap^a_ir_a\) is then split by \[P\xrightarrow{q^a_ir_a}X^a_i \xrightarrow{s_am^a_i}P.\] Thus realization sends the block indexed by \((a,i)\) to \(X^a_i\). The realized component of the injection is \[(q^a_ir_a)(s_ap^a_i)m^a_i = q^a_ip^a_im^a_i = 1_{X^a_i}.\] Hence the realized object is the concatenation of the realized families and the realized injections are the ordinary family coproduct injections.

12.4 Explicit realization and presentation↩︎

The equivalence has a useful concrete description. Let \[E=((I,P),(u,p))\] be a completed constant family. For each \(i\in I_0:=\operatorname{Fix}(u)\), choose a splitting \[P\xrightarrow{q_i}P_i\xrightarrow{m_i}P, \qquad m_iq_i=p_i, \quad q_im_i=1.\] Then \[\mathfrak R(E)=(P_i)_{i\in I_0}.\] If \((f,\phi):E\to F\) is a Karoubi arrow, then \(f\) restricts to a function \(\operatorname{Fix}(u)\to\operatorname{Fix}(v)\) and the realized component at \(i\) is \[q^F_{f(i)}\phi_i m^E_i.\] Thus realization replaces each ambient projector by its splitting object and restricts each ambient arrow to the corresponding images.

Conversely, choose for every family \(X=(X_i)_{i\in I}\) a common host \[X_i\xrightarrow{s_i^X}P_X\xrightarrow{r_i^X}X_i.\] Its ambient presentation is \[\mathfrak P(X)= \left( (I,P_X), \bigl(1_I,(s_i^Xr_i^X)_{i\in I}\bigr) \right).\] A family arrow \((f,\alpha):X\to Y\) is represented by \[\mathfrak P(f,\alpha) = \left( f, (s^Y_{f(i)}\alpha_i r_i^X)_{i\in I} \right).\] The retraction equations make these formulas functorial: the middle factors cancel under composition, and the ambient representative of an identity is the corresponding projector.

In the concrete case \(\mathcal{C}=\mathbf{Vect}^{\mathrm{op}}\), a family \((V_i)_{i\in I}\) may be presented on the single ambient vector space \(\bigoplus_iV_i\), with the coordinate projectors selecting the valid fibre. Splitting those projectors recovers the original family. This is the precise sense in which a dependent cotangent family and a simply typed ambient cotangent equipped with primal-indexed projectors are two representations of the same object.

13 Common retract hosts from standard categorical structure↩︎

The common-host hypothesis of 1 is often automatic. This appendix records a general sufficient condition and then specializes it to the examples relevant to the paper. The point is that a host need not be a particular coproduct: either a product or a coproduct can serve, provided that zero morphisms are available.

13.1 General criterion↩︎

This is the combination of [lem:common-hosts-products-coproducts,prop:kar-coprod,thm:criterion]. For a product host, the section into the \(i\)-th coordinate has identity as its \(i\)-th component and zero as every other component. For a coproduct host, the retraction from the \(i\)-th summand is identity on that summand and zero on all others. Different choices of hosts generally give different ambient presentations, but the resulting coproduct objects in the Karoubi completion are isomorphic by the coproduct universal property.

13.2 Vector spaces and their opposite↩︎

The categories \(\mathbf{Vect}\) and \(\mathbf{Vect}^{\mathrm{op}}\) are Cauchy complete, have zero objects, and admit all small products and coproducts. Hence \[\mathsf{Kar}\bigl(\mathsf{Copow}_\kappa(\mathbf{Vect})\bigr) \simeq \mathsf{Fam}_\kappa(\mathbf{Vect})\] and \[\mathsf{Kar}\bigl(\mathsf{Copow}_\kappa(\mathbf{Vect}^{\mathrm{op}})\bigr) \simeq \mathsf{Fam}_\kappa(\mathbf{Vect}^{\mathrm{op}}).\]

For a family \((V_i)_{i\in I}\) in \(\mathbf{Vect}^{\mathrm{op}}\), either of the following may be used as a common host.

1. The direct sum \(P_\oplus=\bigoplus_iV_i\) in \(\mathbf{Vect}\), regarded as a product in \(\mathbf{Vect}^{\mathrm{op}}\). The coordinate projection \(\pi_i:P_\oplus\to V_i\) in \(\mathbf{Vect}\) represents the section \(V_i\to P_\oplus\) in \(\mathbf{Vect}^{\mathrm{op}}\), while the coordinate injection \(\iota_i:V_i\to P_\oplus\) represents the retraction.

2. The direct product \(P_\Pi=\prod_iV_i\) in \(\mathbf{Vect}\), regarded as a coproduct in \(\mathbf{Vect}^{\mathrm{op}}\). The product projection represents the coproduct injection in \(\mathbf{Vect}^{\mathrm{op}}\), while the one-coordinate map \(\delta_i:V_i\to P_\Pi\) represents its retraction.

For finite families these hosts agree up to the canonical biproduct isomorphism. For infinite families they generally differ. We use direct sums because they give the sparse, finitely supported ambient representation. With this choice, a family arrow whose backward components are \(\alpha_i^*:Y_{f(i)}\to X_i\) is represented on the \(i\)-th block by \[P_Y \xrightarrow{\pi_{f(i)}} Y_{f(i)} \xrightarrow{\alpha_i^*} X_i \xrightarrow{\iota_i} P_X,\] namely by \(\iota_i\alpha_i^*\pi_{f(i)}\).

13.3 Modules and additive categories↩︎

Let \(R\) be a ring. The categories \(R\text{-}\mathbf{Mod}\) and \((R\text{-}\mathbf{Mod})^{\mathrm{op}}\) are Cauchy complete, have zero objects, and admit all small products and coproducts. Therefore the same two completion equivalences hold for modules. More generally, any Cauchy-complete category with zero morphisms and the required products or coproducts satisfies [prop:standard-hosts-app]. In particular, this applies to Cauchy-complete additive categories whenever the relevant products or coproducts exist; finite biproducts automatically provide hosts for finite families.

13.4 Pointed sets and sparse tagged carriers↩︎

The category \(\mathbf{Set}_{*}\) of pointed sets is Cauchy complete, has a zero object, and admits all small products and coproducts. Thus \[\mathsf{Kar}\bigl(\mathsf{Copow}_\kappa(\mathbf{Set}_{*}^{\mathrm{op}})\bigr) \simeq \mathsf{Fam}_\kappa(\mathbf{Set}_{*}^{\mathrm{op}}).\] A convenient host for a family of pointed sets \((X_i,*)\) is the wedge \[P=\bigvee_{i\in I}X_i.\] The inclusion of the \(i\)-th summand has a pointed retraction that is the identity on that summand and collapses every other summand to the basepoint. After passage to the opposite category, these maps give the required section and retraction. For two branches, the wedge has the shape “zero, a left payload, or a right payload”, and the projectors collapse the unselected branch to zero. This explains the carrier shape of a sparse tagged implementation, although pointed sets themselves do not supply the linear accumulation or transposed derivatives required for cotangent semantics.

14 Explicit structure of the completed constant-cotangent model↩︎

This appendix gives the bicartesian closed structure explicitly. Expressive CHAD proves that \(\mathsf{Fam}(\mathbf{Vect}^{\mathrm{op}})\) is bicartesian closed and identifies it as the concrete reverse-mode target [6, Sec. 10.2], Corollary 82, and Equation (68). Together with 1, this already gives a bicartesian closed structure on \(\mathsf{Kar}(\mathsf{Copow}(\mathbf{Vect}^{\mathrm{op}}))\) by transport across realization. The purpose of this appendix is to describe the terminal object, products, the initial object, coproducts, exponentials, evaluation, and currying directly on ambient constant-cotangent objects and to identify their images under realization.

Put \[\mathcal{K}=\mathsf{Kar}(\mathsf{Copow}(\mathbf{Vect}^{\mathrm{op}})), \qquad \mathcal{F}=\mathsf{Fam}(\mathbf{Vect}^{\mathrm{op}}).\]

We now give the explicit ambient account.

14.1 Objects, arrows, and realization↩︎

An object of \(\mathcal{K}\) is written \[E=((A,V),e), \qquad e=(r,p),\] where \(r:A\to A\) and \(p_a:V\to V\) satisfy \[r^2=r, \qquad p_a p_{r(a)}=p_a.\] Let \[F=((B,W),d), \qquad d=(s,q).\] A morphism \(h:E\to F\) is represented by a function \(h_0:A\to B\) and linear maps \(h_a^*:W\to V\) satisfying \[h_0=s h_0 r, \qquad h_a^*=p_a h_{r(a)}^*q_{h_0(r(a))}. \label{eq:kar-arrow-components}\tag{1}\] These are precisely the component equations for \(h=dhe\).

For \(a\in A_0:=\operatorname{Fix}(r)\), \(p_a\) is an idempotent. Write its image splitting as \[V_a^0=\operatorname{im}(p_a), \qquad V_a^0\xrightarrow{\iota_a^E}V\xrightarrow{\rho_a^E}V_a^0,\] with \[\rho_a^E\iota_a^E=1, \qquad \iota_a^E\rho_a^E=p_a.\] Then \[\mathfrak R(E)=(V_a^0)_{a\in A_0}.\] If \(h:E\to F\), the first equation in 1 restricts \(h_0\) to a function \(A_0\to B_0:=\operatorname{Fix}(s)\), and the realized backward map is \[(\mathfrak Rh)_a^* = \rho_a^E h_a^*\iota_{h_0(a)}^F: W_{h_0(a)}^0\longrightarrow V_a^0. \label{eq:realized-arrow-components}\tag{2}\]

14.2 Arbitrary small coproducts in the completed model↩︎

Let \((E_a)_{a\in A}\) be a small family of objects in \(\mathcal{K}\), with \[E_a=\bigl((I_a,V_a),(r_a,p^a)\bigr).\] Put \[I=\coprod_{a\in A}I_a, \qquad P=\bigoplus_{a\in A}V_a,\] and write \(\jmath_a:V_a\to P\) and \(\pi_a:P\to V_a\) for the coordinate maps in \(\mathbf{Vect}\). Define \(c=(r,p)\) on \((I,P)\) by \[\begin{align} r(\mathsf{in}_a(i)) &=\mathsf{in}_a(r_a(i)),\\ p_{\mathsf{in}_a(i)} &=\jmath_a p^a_i\pi_a:P\longrightarrow P. \end{align} \label{eq:arbitrary-vect-coproduct}\tag{3}\] Since the reverse-target composition law gives \[(p\circ p)_{\mathsf{in}_a(i)} = p_{\mathsf{in}_a(i)}p_{r(\mathsf{in}_a(i))},\] we have \[\jmath_a p^a_i\pi_a\jmath_a p^a_{r_a(i)}\pi_a = \jmath_a p^a_i p^a_{r_a(i)}\pi_a = \jmath_a p^a_i\pi_a.\] Thus \(c\) is idempotent.

The injection \(\iota_a:E_a\to((I,P),c)\) is \[(\iota_a)_0(i)=\mathsf{in}_a(r_a(i)), \qquad (\iota_a)^*_i=p^a_i\pi_a:P\longrightarrow V_a. \label{eq:arbitrary-vect-injection}\tag{4}\] Let \(H=((J,W),(s,q))\) and let \(h_a:E_a\to H\) be Karoubi arrows. Define \[[h_a]_{a\in A,0}(\mathsf{in}_a(i))=h_{a,0}(i), \qquad [h_a]_{a\in A,\mathsf{in}_a(i)}^* =\jmath_a h_{a,i}^*:W\longrightarrow P. \label{eq:arbitrary-vect-copairing}\tag{5}\] The target compatibility of each \(h_a\) and its source compatibility with \((r_a,p^a)\) imply the sandwich equation for 5 . Its composite with 4 has primal component \[h_{a,0}(r_a(i))=h_{a,0}(i)\] and backward component \[p^a_i\pi_a\jmath_a h^*_{a,r_a(i)} = p^a_i h^*_{a,r_a(i)} = h^*_{a,i}.\] Hence \([h_a]_{a\in A}\iota_a=h_a\). Conversely, if \(k:((I,P),c)\to H\) has these composites, the equation \(k=kc\) restricts its backward map on the \(a\)-th block to the image of \(\jmath_a p^a_i\pi_a\), while \(k\iota_a=h_a\) fixes that restriction as \(\jmath_a h^*_{a,i}\). The direct-sum universal property then forces 5 ; the primal component is forced branchwise as well. Thus \(((I,P),c)\) is the coproduct of the \(E_a\). For \(A=\varnothing\), this gives \(((\varnothing,0),1)\).

As expected, realization sends this object to the concatenated family \[\bigl(\operatorname{im}(p^a_i)\bigr)_{a\in A,\;i\in\operatorname{Fix}(r_a)},\] because the image of \(\jmath_a p^a_i\pi_a\) is canonically isomorphic to \(\operatorname{im}(p^a_i)\). Under these isomorphisms the displayed injections and copairing become the standard family coproduct maps.

14.3 Initial object and binary coproducts↩︎

The bicartesian closed structure of \(\mathcal{K}\) is the structure used by the program semantics. The initial object of \(\mathcal{K}\) is \[0_{\mathcal{K}}=((\varnothing,0),1).\] There is a unique ambient arrow from it to every object, so it is also initial in the Karoubi envelope.

Let \[E=((A,V),(r,p)), \qquad F=((B,W),(s,q)).\] Their coproduct is \[E+F = \left( (A+B,V\oplus W),c_{E,F} \right), \label{eq:kar-coproduct-concrete}\tag{6}\] where \[\begin{align} (c_{E,F})_0(\mathsf{inl}(a))&=\mathsf{inl}(r(a)), & (c_{E,F})^*_{\mathsf{inl}(a)}(v,w)&=(p_a(v),0),\\ (c_{E,F})_0(\mathsf{inr}(b))&=\mathsf{inr}(s(b)), & (c_{E,F})^*_{\mathsf{inr}(b)}(v,w)&=(0,q_b(w)). \end{align}\] The equations for \(e\) and \(d\) show branchwise that \(c_{E,F}^2=c_{E,F}\).

The injections are \[\iota_E:E\longrightarrow E+F, \qquad \iota_F:F\longrightarrow E+F,\] with \[(\iota_E)_0(a)=\mathsf{inl}(r(a)), \qquad (\iota_E)_a^*(v,w)=p_a(v),\] \[(\iota_F)_0(b)=\mathsf{inr}(s(b)), \qquad (\iota_F)_b^*(v,w)=q_b(w).\] These are precisely the ambient injections sandwiched by the source and coproduct idempotents.

The realization equivalence sends this coproduct to the branchwise family coproduct because \[\operatorname{Fix}((c_{E,F})_0)=\operatorname{Fix}(r)+\operatorname{Fix}(s),\] and the projector images on the left and right branches are respectively \(\operatorname{im}(p_a)\) and \(\operatorname{im}(q_b)\). The realized injections and copairing are the standard family ones.

14.4 Terminal object and binary products↩︎

Let \[E=((A,V),(r,p)), \qquad F=((B,W),(s,q))\] be objects of \(\mathcal{K}\). The terminal object is \[1_{\mathcal{K}}=((1,0),1).\] There is a unique ambient arrow from every object to \((1,0)\), and it satisfies every sandwich equation because its backward component has domain \(0\).

The product is \[E\times F = \left( (A\times B,V\oplus W), (r\times s,p\oplus q) \right), \label{eq:kar-product}\tag{7}\] where \[(r\times s)(a,b)=(r(a),s(b)),\] \[(p\oplus q)_{(a,b)}(v,w)=(p_a(v),q_b(w)).\] Its projections are \[\pi_E:E\times F\longrightarrow E, \qquad \pi_F:E\times F\longrightarrow F,\] with primal components \[(\pi_E)_0(a,b)=r(a), \qquad (\pi_F)_0(a,b)=s(b),\] and backward components \[(\pi_E)^*_{(a,b)}(v)=(p_a(v),0), \qquad (\pi_F)^*_{(a,b)}(w)=(0,q_b(w)).\] They satisfy the sandwich equations directly.

Let \[G=((C,U),(t,\ell))\] and let \(h:G\to E\) and \(k:G\to F\). Define \[\langle h,k\rangle_0(c)=(h_0(c),k_0(c))\] and \[\langle h,k\rangle_c^*(v,w) =h_c^*(v)+k_c^*(w). \label{eq:kar-product-pairing}\tag{8}\] The sandwich equations for \(h\) and \(k\) imply \[\langle h,k\rangle =(e\times d)\langle h,k\rangle(t,\ell),\] so this is a Karoubi arrow. Moreover, \[\pi_E\langle h,k\rangle=h, \qquad \pi_F\langle h,k\rangle=k,\] because target compatibility gives \(h_c^*p_{h_0(c)}=h_c^*\) and \(k_c^*q_{k_0(c)}=k_c^*\).

For uniqueness, suppose \(m:G\to E\times F\) has these two composites. The projection equations force \[m_0(c)=(h_0(c),k_0(c)).\] Writing \(m_c^*:V\oplus W\to U\), the same equations determine its restrictions to the two biproduct summands: \[m_c^*(v,0)=h_c^*(v), \qquad m_c^*(0,w)=k_c^*(w).\] Linearity therefore forces 8 . This proves the product universal property.

As expected, realization preserves this product through the canonical isomorphisms \[\operatorname{Fix}(r\times s)=\operatorname{Fix}(r)\times\operatorname{Fix}(s),\] \[\operatorname{im}(p_a\oplus q_b) \cong \operatorname{im}(p_a)\oplus\operatorname{im}(q_b).\] Under these isomorphisms the realized projections and pairing are the standard family projections and pairing.

14.5 The standard dependent-family structure↩︎

We first record the structure to which the ambient formulas will be compared. We recall the structure of \(\mathcal{F}\), see [6]. Let \[X=(V_a)_{a\in A}, \qquad Y=(W_b)_{b\in B}\] be objects of \(\mathcal{F}\). The terminal object and binary product are \[1_{\mathcal{F}}=(0)_{*\in1}, \qquad X\times Y=(V_a\oplus W_b)_{(a,b)\in A\times B}.\] The initial object is the empty family, and the binary coproduct is branchwise: \[0_{\mathcal{F}}=()_{c\in\varnothing}, \qquad X+Y=(Z_c)_{c\in A+B},\] where \[Z_{\mathsf{inl}(a)}=V_a, \qquad Z_{\mathsf{inr}(b)}=W_b.\]

For the exponential, define \[\mathsf H(X,Y)= \left\{ (f,\phi)\;\middle|\; \begin{array}{l} f:A\to B,\\[-1mm] \phi_a:W_{f(a)}\to V_a\text{ linear for all }a\in A \end{array} \right\}.\] For \((f,\phi)\in\mathsf H(X,Y)\), put \[K_{(f,\phi)}=\bigoplus_{a\in A}W_{f(a)}.\] Then \[Y^X= \bigl(K_{(f,\phi)}\bigr)_{(f,\phi)\in\mathsf H(X,Y)}. \label{eq:fam-exponential}\tag{9}\] The evaluation arrow has primal component \[\mathsf{ev}_0((f,\phi),a)=f(a)\] and backward component \[\mathsf{ev}_{((f,\phi),a)}^*(w) = \bigl(\jmath_a(w),\phi_a(w)\bigr): W_{f(a)}\longrightarrow K_{(f,\phi)}\oplus V_a, \label{eq:fam-evaluation}\tag{10}\] where \(\jmath_a\) is the \(a\)-th direct-sum injection.

For completeness, let \(Z=(U_c)_{c\in C}\) and let \(k:Z\times X\to Y\). Write its backward component as \[k_{c,a}^*=\langle k^U_{c,a},k^V_{c,a}\rangle: W_{k_0(c,a)}\longrightarrow U_c\oplus V_a.\] Its transpose sends \(c\) to \[\left( a\longmapsto k_0(c,a), (k^V_{c,a})_{a\in A} \right)\in\mathsf H(X,Y),\] and its backward component \[\bigoplus_{a\in A}W_{k_0(c,a)}\longrightarrow U_c\] has restriction \(k^U_{c,a}\) to the \(a\)-th summand. Evaluation recovers \(k_0\), \(k^U\), and \(k^V\). Hence these operations are mutually inverse and natural, proving the exponential adjunction in \(\mathcal{F}\).

14.6 The ambient exponential and its Karoubi idempotent↩︎

The ambient category \(\mathsf{Copow}(\mathbf{Vect}^{\mathrm{op}})\) is cartesian closed; the following formulas are the concrete constant-cotangent instance of basic higher-order CHAD [4], [5]. Its exponential from \((A,V)\) to \((B,W)\) has primal set \[H= \left\{ (f,\phi)\;\middle|\; f:A\to B, \;\phi_a:W\to V\text{ linear for all }a\in A \right\}\] and cotangent space \[Z=\bigoplus_{a\in A}W.\] Let \(\jmath_a:W\to Z\) be the direct-sum injections. Ambient evaluation has primal component \[\mathsf{ev}_0((f,\phi),a)=f(a)\] and backward component \[\mathsf{ev}_{((f,\phi),a)}^*(w) = (\jmath_a(w),\phi_a(w)): W\longrightarrow Z\oplus V. \label{eq:ambient-evaluation}\tag{11}\] The ordinary currying operation is obtained by decomposing a backward map into its \(Z\)- and \(V\)-components and using the direct-sum universal property.

The standard fact that the Karoubi envelope of a cartesian-closed category is cartesian closed belongs to the classical Karoubi/semifunctor theory [17], [18]; see also the general Cauchy-completion background in [9]. Here we need its concrete form. Define \[\varepsilon_{E,F}:(H,Z)\longrightarrow(H,Z)\] by \[(\varepsilon_{E,F})_0(f,\phi) = \left( s f r, \bigl(p_a\phi_{r(a)}q_{f(r(a))}\bigr)_{a\in A} \right) \label{eq:exponential-idempotent-base}\tag{12}\] and by the unique backward map satisfying \[(\varepsilon_{E,F})^*_{(f,\phi)}\jmath_a = \jmath_{r(a)}q_{f(r(a))} \qquad(a\in A). \label{eq:exponential-idempotent-back}\tag{13}\] This is the transpose of \[(H,Z)\times(A,V) \xrightarrow{1\times e} (H,Z)\times(A,V) \xrightarrow{\mathsf{ev}} (B,W) \xrightarrow{d} (B,W).\] Equivalently, it is the internal operation \[h\longmapsto dhe.\] It is therefore idempotent. Directly, the base calculation uses \(r^2=r\), \(s^2=s\), \(p_ap_{r(a)}=p_a\), and \(q_bq_{s(b)}=q_b\); the backward calculation follows by checking every direct-sum injection in 13 .

The exponential in \(\mathcal{K}\) is \[F^E=((H,Z),\varepsilon_{E,F}). \label{eq:kar-exponential}\tag{14}\] Its evaluation is the restricted ambient evaluation \[\mathsf{ev}_{E,F} = d\,\mathsf{ev}\,(\varepsilon_{E,F}\times e).\] At an ambient point \(((f,\phi),a)\), its primal component is \[s(f(r(a)))\] and its backward component is \[w\longmapsto \left( \jmath_{r(a)}q_{f(r(a))}(w), p_a\phi_{r(a)}q_{f(r(a))}(w) \right). \label{eq:kar-evaluation-explicit}\tag{15}\]

Let \[G=((C,U),t)\] and let \(k:G\times E\to F\) be a Karoubi arrow. Write its ambient backward map as \[k_{c,a}^*=\langle k^U_{c,a},k^V_{c,a}\rangle.\] Its ambient transpose has primal component \[c\longmapsto \left( a\longmapsto k_0(c,a), (k^V_{c,a})_{a\in A} \right)\] and backward component \(Z\to U\) whose restriction to the \(a\)-th summand is \(k^U_{c,a}\). The ambient exponential adjunction transports the sandwich equation exactly as follows: \[k=d\,k\,(t\times e) \quad\Longleftrightarrow\quad \Lambda(k)=\varepsilon_{E,F}\,\Lambda(k)\,t.\] Hence \(\Lambda(k)\) is a Karoubi arrow \(G\to F^E\). Conversely, restricted evaluation uncarries every Karoubi arrow \(G\to F^E\). Since these are the ordinary mutually inverse currying operations, they are natural and satisfy the triangle equations. This proves the exponential universal property.

14.7 Explicit comparison of the exponentials↩︎

Put \[A_0=\operatorname{Fix}(r), \qquad B_0=\operatorname{Fix}(s), \qquad V_a^0=\operatorname{im}(p_a), \qquad W_b^0=\operatorname{im}(q_b).\] The base set of \(\mathfrak R(F)^{\mathfrak R(E)}\) consists of pairs \[(g,\bar\phi), \qquad g:A_0\to B_0, \qquad \bar\phi_a:W_{g(a)}^0\to V_a^0.\] There is a bijection \[\Theta: \operatorname{Fix}((\varepsilon_{E,F})_0) \longrightarrow \mathsf H(\mathfrak R(E),\mathfrak R(F)) \label{eq:exponential-base-comparison}\tag{16}\] given by \[\Theta(f,\phi) = \left( f|_{A_0}, (\rho_a^E\phi_a\iota_{f(a)}^F)_{a\in A_0} \right).\] The inverse bijection sends \((g,\bar\phi)\) to \((\widetilde{g},\widetilde{\phi})\), where \[\widetilde{g}(a)=g(r(a)),\] \[\widetilde{\phi}_a = p_a\iota_{r(a)}^E \bar\phi_{r(a)} \rho_{g(r(a))}^F.\] The fixed-point equations in 12 show directly that the two assignments are inverse.

Fix \((f,\phi)\in\operatorname{Fix}((\varepsilon_{E,F})_0)\) and put \[K_{(f,\phi)}^0 = \bigoplus_{a\in A_0}W_{f(a)}^0.\] This is the fibre of the family exponential at \(\Theta(f,\phi)\). Define \[K_{(f,\phi)}^0 \xrightarrow{\iota_{(f,\phi)}^{\Rightarrow}} Z \xrightarrow{\rho_{(f,\phi)}^{\Rightarrow}} K_{(f,\phi)}^0\] by \[\iota_{(f,\phi)}^{\Rightarrow}\jmath_a^0 = \jmath_a\iota_{f(a)}^F \qquad(a\in A_0),\] \[\rho_{(f,\phi)}^{\Rightarrow}\jmath_a = \jmath_{r(a)}^0\rho_{f(r(a))}^F \qquad(a\in A).\] Then \[\rho_{(f,\phi)}^{\Rightarrow} \iota_{(f,\phi)}^{\Rightarrow}=1,\] and \[\iota_{(f,\phi)}^{\Rightarrow} \rho_{(f,\phi)}^{\Rightarrow} =(\varepsilon_{E,F})^*_{(f,\phi)}.\] The second equation follows by evaluating both maps on each \(\jmath_a\) and using 13 . Thus realization of the ambient exponential fibre gives precisely the family exponential fibre.

Under the base bijection and these splittings, realization of 15 is the family evaluation 10 . Indeed, for fixed \((f,\phi)\), fixed \(a\in A_0\), and \(w\in W_{f(a)}^0\), the realized backward map is \[w\longmapsto \left( \jmath_a^0(w), \rho_a^E\phi_a\iota_{f(a)}^F(w) \right).\] The first component is the cotangent contribution to the function object and the second is the realized backward map at \(a\). Since realization identifies evaluation, it also identifies currying by uniqueness of transposes.

15 Finite coproducts in the completed reverse target↩︎

We now pass from the constant-family theorem to the ordinary reverse target of basic CHAD. The cartesian-closed part of the argument is already available: basic CHAD proves that the total reverse category is cartesian closed, and Karoubi completion preserves cartesian closure. The only new task is therefore to construct the finite coproducts required by variants.

15.1 Inherited cartesian closure↩︎

Let \[\mathsf T_{\mathsf{Tar}}^{\leftarrow}=\Sigma_{\mathsf C_{\mathsf{Tar}}}\mathsf L_{\mathsf{Tar}}^{\mathrm{op}}\] be the ordinary reverse target. We assume that \((\mathsf C_{\mathsf{Tar}},\mathsf L_{\mathsf{Tar}})\) is a categorical model of the basic CHAD target language in the sense of [5]. In particular, \(\mathsf L_{\mathsf{Tar}}\) is locally indexed, its fibres have chosen finite biproducts preserved by reindexing, and it supports cartesian linear-function objects. By [5], \(\mathsf T_{\mathsf{Tar}}^{\leftarrow}\) is cartesian closed. For variants, we assume only that \(\mathsf C_{\mathsf{Tar}}\) has finite coproducts.

This is the standard cartesian-closed structure on the Karoubi completion; see [17], [18]. Applying it to \(\mathsf T_{\mathsf{Tar}}^{\leftarrow}\) shows that \(\mathsf{Kar}(\mathsf T_{\mathsf{Tar}}^{\leftarrow})\) is already cartesian closed. We now construct its finite coproducts from the structure already present in the basic CHAD target.

15.2 Common hosts and branchwise linear maps↩︎

Thus the two pieces of structure that might otherwise appear as additional variant assumptions are already available: the fibrewise biproducts give the common hosts, while the cartesian linear-function objects derive branchwise linear case analysis from finite coproducts in \(\mathsf C_{\mathsf{Tar}}\).

15.3 Finite coproducts after completion↩︎

Let \[E=((A,V),e), \qquad F=((B,W),d),\] where \(e=(r,p)\) and \(d=(s,q)\) are idempotent endomorphisms in \(\mathsf T_{\mathsf{Tar}}^{\leftarrow}\). Put \(P=V\oplus W\). Define an endomorphism \(c_{E,F}\) of \((A+B,P)\) by \[\begin{align} c_{E,F,1}(\mathsf{inl}(a)) &=\mathsf{inl}(r(a)), & (c_{E,F})^*_{\mathsf{inl}(a)}(v,w) &=(p_a(v),0),\\ c_{E,F,1}(\mathsf{inr}(b)) &=\mathsf{inr}(s(b)), & (c_{E,F})^*_{\mathsf{inr}(b)}(v,w) &=(0,q_b(w)). \end{align}\] The backward component exists uniquely by 12. Since \[r^2=r, \qquad p_a\circ p_{r(a)}=p_a, \qquad s^2=s, \qquad q_b\circ q_{s(b)}=q_b,\] the same branchwise calculation gives \[c_{E,F}^2=c_{E,F}.\] Set \[E+F:=((A+B,V\oplus W),c_{E,F}).\]

Let \[j_E:(A,V)\longrightarrow(A+B,V\oplus W), \qquad j_F:(B,W)\longrightarrow(A+B,V\oplus W)\] be the ambient injections. Their primal components are \(\mathsf{inl}\) and \(\mathsf{inr}\), and their backward components are the corresponding biproduct projections. Define the completed injections by \[\iota_E=c_{E,F}\circ j_E\circ e, \qquad \iota_F=c_{E,F}\circ j_F\circ d.\] Explicitly, \[(\iota_E)_1=\mathsf{inl}\circ r, \qquad (\iota_E)^*_a(v,w)=p_a(v),\] and \[(\iota_F)_1=\mathsf{inr}\circ s, \qquad (\iota_F)^*_b(v,w)=q_b(w).\]

16 The simply typed reverse-mode transformation↩︎

Bicartesian closure determines the transformation abstractly, following the semantics-driven methodology of basic and expressive CHAD [4]–[6]. This section unfolds the new data-type clauses into executable nondependent target terms and records the categorical form of the higher-order clauses. The displayed term rules below are for data-type contexts and results, where the primal component of every generated idempotent is the identity. For arbitrary higher-order contexts, structural maps must instead be restricted by the full source and target idempotents. The invariant throughout is the sandwich equation: each generated map restricts to the valid projector image at its source and lands in the valid image at its target. The presentation also separates this semantic derivation from subsequent implementation optimisations such as sparse accumulation and closure conversion [8].

16.1 Types, ambient cotangents, and projectors↩︎

For clarity, we spell out the clauses that are new for variants or modified by the generated projectors. The data types of the present source fragment are \[\tau,\sigma::= \mathsf{real}^n \mid 1 \mid \tau\times\sigma \mid 0 \mid \tau+\sigma.\] For each type, the translation produces a primal type \(\widehat D_1\tau\), an ambient cotangent type \(\widehat D_2\tau\), and a primal-indexed projector \[p_\tau: \widehat D_1\tau; \widehat D_2\tau \multimap \widehat D_2\tau.\] At ground types and the unit type, \[\widehat D_1(\mathsf{real}^n)=\mathsf{real}^n, \qquad \widehat D_2(\mathsf{real}^n)=\mathsf{real}^n, \qquad p_{\mathsf{real}^n}(x,v)=v,\] \[\widehat D_1(1)=1, \qquad \widehat D_2(1)=0, \qquad p_1(*,0)=0.\] For products, \[\begin{align} \widehat D_1(\tau\times\sigma) &=\widehat D_1\tau\times\widehat D_1\sigma,\\ \widehat D_2(\tau\times\sigma) &=\widehat D_2\tau\oplus\widehat D_2\sigma,\\ p_{\tau\times\sigma}((x,y),(v,w)) &=(p_\tau(x,v),p_\sigma(y,w)). \end{align}\] For sums, \[\begin{align} \widehat D_1(\tau+\sigma) &=\widehat D_1\tau+\widehat D_1\sigma,\\ \widehat D_2(\tau+\sigma) &=\widehat D_2\tau\oplus\widehat D_2\sigma,\\ p_{\tau+\sigma}(\mathsf{inl}(x),(v,w)) &=(p_\tau(x,v),0),\\ p_{\tau+\sigma}(\mathsf{inr}(y),(v,w)) &=(0,p_\sigma(y,w)). \end{align}\] The empty type has no primal values, so its projector has no branch to define. For a context \[\Gamma=x_1:\tau_1,\ldots,x_n:\tau_n,\] put \(\widehat D_2\Gamma=\bigoplus_i\widehat D_2\tau_i\) and let \(p_\Gamma(\gamma,-)\) act componentwise at the primal environment \(\gamma\). We write \(\mathsf{one}_i:\widehat D_2\tau_i\multimap\widehat D_2\Gamma\) for the \(i\)-th biproduct injection.

16.2 Clauses for data-type constructors↩︎

For a judgement \(\Gamma\vdash t:\tau\) in the data-type fragment, the transformation produces \[\widehat D_1\Gamma\vdash \overleftarrow D_\Gamma(t): \widehat D_1\tau \times (\widehat D_2\tau\multimap\widehat D_2\Gamma).\] Write \(0\) and \(+\) for cotangent zero and addition. The standard CHAD clauses are sandwiched by the generated projectors. We display the projector-modified structural clauses and then give the variant clauses in full; primitive clauses not affected by variants are inherited from basic CHAD [5]. The displayed variable clause is valid because all types in \(\Gamma\) are data types. In an arbitrary higher-order context, let \(e_\Gamma\) denote the product idempotent on the translated context. The structural arrow is the full Karoubi restriction \[\overleftarrow{\mathcal{D}}_{\mathrm{st}}(x_i)=e_{\tau_i}\,\pi_i\,e_\Gamma.\] Thus, for a one-variable context, the erased translation of the identity is \(e_\tau\), not the ambient identity. Its data-type specialization is \[\overleftarrow D_\Gamma(x_i) = \left\langle x_i, \lambda\bar x.\mathsf{one}_i(p_{\tau_i}(x_i,\bar x)) \right\rangle,\] \[\overleftarrow D_\Gamma(\langle\rangle) = \langle\langle\rangle,\lambda\bar u.0\rangle,\] \[\begin{align} \overleftarrow D_\Gamma(\langle t,s\rangle) ={}& \mathbf{let}\;\langle x,x^*\rangle=\overleftarrow D_\Gamma(t)\;\mathbf{in}\\ &\mathbf{let}\;\langle y,y^*\rangle=\overleftarrow D_\Gamma(s)\;\mathbf{in}\\ &\left\langle \langle x,y\rangle, \lambda(\bar x,\bar y). x^*(p_\tau(x,\bar x))+y^*(p_\sigma(y,\bar y)) \right\rangle, \end{align}\] \[\begin{align} \overleftarrow D_\Gamma(\pi_1t) ={}& \mathbf{let}\;\langle(x,y),h\rangle=\overleftarrow D_\Gamma(t)\;\mathbf{in}\\ &\left\langle x,\lambda\bar x.h(p_\tau(x,\bar x),0)\right\rangle, \end{align}\] with a symmetric clause for \(\pi_2\).

For a primitive operation, use its chosen codifferential and compose on both sides with the generated projectors. For a let-binding, suppose \[\overleftarrow D_\Gamma(t)=\langle x,x^*\rangle, \qquad \overleftarrow D_{\Gamma,x:\tau}(s)=\langle y,y^*\rangle.\] Then \[\begin{align} &\overleftarrow D_\Gamma(\mathbf{let}\;x=t\;\mathbf{in}\;s)\\ ={}& \mathbf{let}\;\langle x,x^*\rangle=\overleftarrow D_\Gamma(t)\;\mathbf{in}\\ &\mathbf{let}\;\langle y,y^*\rangle=\overleftarrow D_{\Gamma,x:\tau}(s)\;\mathbf{in}\\ &\left\langle y, \lambda\bar y. \mathbf{let}\;\langle\bar\gamma,\bar x\rangle =y^*(p_\sigma(y,\bar y))\;\mathbf{in} p_\Gamma(\gamma,\bar\gamma)+x^*(p_\tau(x,\bar x)) \right\rangle. \end{align}\]

For injections, \[\begin{align} \overleftarrow D_\Gamma(\mathsf{inl}\,t) ={}& \mathbf{let}\;\langle x,x^*\rangle=\overleftarrow D_\Gamma(t)\;\mathbf{in}\\ &\left\langle \mathsf{inl}(x), \lambda(v,w).x^*(p_\tau(x,v)) \right\rangle, \end{align}\] \[\begin{align} \overleftarrow D_\Gamma(\mathsf{inr}\,t) ={}& \mathbf{let}\;\langle y,y^*\rangle=\overleftarrow D_\Gamma(t)\;\mathbf{in}\\ &\left\langle \mathsf{inr}(y), \lambda(v,w).y^*(p_\sigma(y,w)) \right\rangle. \end{align}\] The ignored ambient coordinate is discarded.

For \[c= \mathsf{case}\;t\;\mathsf{of}\; \{\mathsf{inl}(x)\mapsto s \mid \mathsf{inr}(y)\mapsto r\},\] the complete clause is \[\begin{align} \overleftarrow D_\Gamma(c) ={}&\mathbf{let}\;\langle z,z^*\rangle= \overleftarrow D_\Gamma(t)\;\mathbf{in}\\ &\mathsf{case}\;z\;\mathsf{of}\\ &\quad\mathsf{inl}(x)\mapsto \mathbf{let}\;\langle u,u^*\rangle= \overleftarrow D_{\Gamma,x:\tau}(s)\;\mathbf{in}\\ &\qquad\left\langle u,\lambda\bar u. \mathbf{let}\;\langle\bar\gamma,\bar x\rangle= u^*(p_\rho(u,\bar u))\;\mathbf{in}\right.\\[-.2em] &\left. p_\Gamma(\gamma,\bar\gamma)+ z^*\bigl(p_{\tau+\sigma}(\mathsf{inl}(x),(p_\tau(x,\bar x),0))\bigr) \right\rangle,\\ &\quad\mathsf{inr}(y)\mapsto \mathbf{let}\;\langle v,v^*\rangle= \overleftarrow D_{\Gamma,y:\sigma}(r)\;\mathbf{in}\\ &\qquad\left\langle v,\lambda\bar v. \mathbf{let}\;\langle\bar\gamma,\bar y\rangle= v^*(p_\rho(v,\bar v))\;\mathbf{in}\right.\\[-.2em] &\left. p_\Gamma(\gamma,\bar\gamma)+ z^*\bigl(p_{\tau+\sigma}(\mathsf{inr}(y),(0,p_\sigma(y,\bar y)))\bigr) \right\rangle. \end{align}\] The scrutinee is evaluated once, only the selected branch is differentiated, and the branch cotangent is inserted into the ambient biproduct before the scrutinee backpropagator is called. Idempotence simplifies the nested projector to the expected branch insertion. The abort term is the unique map induced by the initial completed object.

16.3 Higher-order types↩︎

Function types use the cartesian closed structure of \(\mathsf{Kar}(\mathsf T_{\mathsf{Tar}}^{\leftarrow})\). If the domain and codomain are represented by full idempotents \(e_\tau\) and \(e_\sigma\), then \[e_{\tau\Rightarrow\sigma}=\varepsilon_{e_\tau,e_\sigma},\] where the exponential idempotent acts internally by \[h\longmapsto e_\sigma h e_\tau.\] The ambient primal and cotangent types are those of basic higher-order CHAD, but the primal component of \(e_{\tau\Rightarrow\sigma}\) generally projects an ambient function–backpropagator package and is not the identity. The concrete base and backward components in the constant-cotangent model are given by 12 and 13 . For arbitrary contexts, every structural arrow is similarly sandwiched by the full context and result idempotents. In particular, abstraction is restricted currying and application is restricted evaluation: \[\operatorname{ev}_{e_\tau,e_\sigma} = e_\sigma\,\operatorname{ev}(\varepsilon_{e_\tau,e_\sigma}\times e_\tau), \qquad \Lambda_{e_\tau,e_\sigma}(f)=\varepsilon_{e_\tau,e_\sigma}\Lambda(f).\] These are the operations described in 15. Hence the higher-order clauses do not reuse the data-type variable rule: they are forced by cartesian closedness and use the full idempotents, as required by [prop:semi].

17 Correctness by comparison with dependent CHAD↩︎

This appendix supplies the concrete comparison used in [prop:standard-target-compatibility,thm:comparison] and expands the proof of 4.

17.1 Concrete realization and preservation↩︎

Recall the concrete-model assumption of 5. The primal functor \(\mathcal{S}:\mathsf C_{\mathsf{Tar}}\to\mathbf{Set}\) and indexed linear functors \(\mathcal{L}_A:\mathsf L_{\mathsf{Tar}}(A)\to\mathbf{Vect}^{\mathcal{S} A}\) induce \[\llbracket-\rrbracket_\mathsf{Tar}:\mathsf T_{\mathsf{Tar}}^{\leftarrow}\longrightarrow\mathsf{Copow}(\mathbf{Vect}^{\mathrm{op}}),\] and therefore \[\llbracket-\rrbracket_{\mathrm{cpl}}: \mathsf{Kar}(\mathsf T_{\mathsf{Tar}}^{\leftarrow}) \xrightarrow{\mathsf{Kar}(\llbracket-\rrbracket_\mathsf{Tar})} \mathsf{Kar}(\mathsf{Copow}(\mathbf{Vect}^{\mathrm{op}})) \xrightarrow{\mathfrak R} \mathsf{Fam}(\mathbf{Vect}^{\mathrm{op}}).\] The terminal object, products, and exponentials of \(\mathsf{Kar}(\mathsf T_{\mathsf{Tar}}^{\leftarrow})\) are the standard Karoubi restrictions of the corresponding structure of \(\mathsf T_{\mathsf{Tar}}^{\leftarrow}\). They are preserved by the assumed basic-CHAD comparisons and by the explicit realization comparisons of 8. It remains to check the completed coproduct.

Let \[E=((A,V),(r,p)), \qquad F=((B,W),(s,q)).\] In the following calculation, \(r,s\) denote the functions obtained by applying \(\mathcal{S}\), while \(p_a,q_b\) denote the linear maps obtained by applying the corresponding indexed interpretations. The coproduct idempotent \(c_{E,F}\) has fixed primal points \[\mathsf{inl}(a)\quad(a\in\operatorname{Fix}(r)), \qquad \mathsf{inr}(b)\quad(b\in\operatorname{Fix}(s)).\] At a left fixed point its backward component on \(\mathcal{V} V\oplus\mathcal{V} W\) is \((v,w)\mapsto(p_a(v),0)\), whose image is canonically isomorphic to \(\operatorname{im}(p_a)\). At a right fixed point it is \((v,w)\mapsto(0,q_b(w))\), whose image is canonically isomorphic to \(\operatorname{im}(q_b)\). Consequently, \[\llbracket E+F\rrbracket_{\mathrm{cpl}} \cong \llbracket E\rrbracket_{\mathrm{cpl}} + \llbracket F\rrbracket_{\mathrm{cpl}}.\] Under these image isomorphisms the completed injections and copairing become the family injections and branchwise copairing; the empty coproduct becomes the empty family. This proves [prop:standard-target-compatibility].

Let \(\overleftarrow{\mathcal{D}}_{\mathrm{dep}}:\mathsf{Syn}_{+}\to\mathsf{Fam}(\mathbf{Vect}^{\mathrm{op}})\) be dependent CHAD. Both \(\llbracket-\rrbracket_{\mathrm{cpl}}\overleftarrow{\mathcal{D}}_{\mathrm{Kar}}\) and \(\overleftarrow{\mathcal{D}}_{\mathrm{dep}}\) are bicartesian closed interpretations, and by assumption they agree on every ground type and primitive operation. They satisfy the same declared equations, so the universal property of \(\mathsf{Syn}_{+}\) gives the coherent natural isomorphism of 3.

Every data type in the present grammar is isomorphic, by repeated distributivity, to a finite sum of finite products of Euclidean ground types. The dependent correctness theorem applies to that normal form, and naturality with respect to the structural isomorphisms transports the result back to the original type. Thus the realized backward map is the mathematical transposed derivative on the genuine cotangent fibres.

17.2 The exact ambient formula↩︎

Let \(t:\tau\to\sigma\) have data-type domain and codomain, write \(f=\llbracket t\rrbracket\), and fix the splitting maps \[T^*_\tau(x) \xrightarrow{\iota_{\tau,x}} \widehat T^*_\tau \xrightarrow{\rho_{\tau,x}} T^*_\tau(x), \qquad \rho_{\tau,x}\iota_{\tau,x}=1, \quad \iota_{\tau,x}\rho_{\tau,x}=p_{\tau,x}.\] Let \(h=\widehat R_t(x)\) be the ambient backward map. The comparison with dependent CHAD gives \[\rho_{\tau,x}h\iota_{\sigma,f(x)} = Df(x)^{\mathsf T},\] while the Karoubi equation gives \[h=p_{\tau,x}hp_{\sigma,f(x)}.\] Substituting \(p=\iota\rho\) yields \[\begin{align} h &= \iota_{\tau,x}\rho_{\tau,x} h \iota_{\sigma,f(x)}\rho_{\sigma,f(x)}\\ &= \iota_{\tau,x} Df(x)^{\mathsf T} \rho_{\sigma,f(x)}. \end{align}\] The same calculation proves uniqueness among ambient maps satisfying the restriction and sandwich equations.

For identities, \(h=\iota\rho=p\). For a composite, the adjacent retraction and section cancel because \(\rho\iota=1\). The semifunctor laws are therefore the transport of ordinary derivative functoriality through the retract presentations.

17.3 A branch-sensitive calculation↩︎

Let \[t:\mathbb{R}+(\mathbb{R}\times\mathbb{R})\to\mathbb{R}, \qquad t(\mathsf{inl}(x))=x^2, \qquad t(\mathsf{inr}(y,z))=yz.\] Choose the ambient cotangent \(\mathbb{R}^3\). The left fibre is split by \[\iota_L(a)=(a,0,0), \qquad \rho_L(a,b,c)=a,\] and the right fibre by \[\iota_R(b,c)=(0,b,c), \qquad \rho_R(a,b,c)=(b,c).\] The associated projectors are \(p_L=\iota_L\rho_L\) and \(p_R=\iota_R\rho_R\).

On the left branch, \[D(x\mapsto x^2)(x)^{\mathsf T}(\bar r)=2x\bar r,\] so \[\widehat R_t(\mathsf{inl}(x))(\bar r) = \iota_L(2x\bar r) =(2x\bar r,0,0).\] On the right branch, \[D((y,z)\mapsto yz)(y,z)^{\mathsf T}(\bar r) =(z\bar r,y\bar r),\] and hence \[\widehat R_t(\mathsf{inr}(y,z))(\bar r) = \iota_R(z\bar r,y\bar r) =(0,z\bar r,y\bar r).\] Thus the ambient result is the mathematical derivative on the active fibre, followed by its inclusion into the common cotangent host.

18 The forward-mode dual↩︎

The paper is phrased in reverse mode because backpropagation is the practically dominant application and because the cotangent interpretation makes the implementation problem especially familiar. Semantically, however, the construction is not specific to reverse mode. From the outset, CHAD presents forward and reverse differentiation through fibrewise-dual total categories [4]–[6]. The present construction therefore applies to forward mode by choosing the Grothendieck construction before, rather than after, taking fibrewise opposites.

Let \[\mathsf T_{\mathsf{Tar}}^{\rightarrow}=\Sigma_{\mathsf C_{\mathsf{Tar}}}\mathsf L_{\mathsf{Tar}}\] be the ordinary forward target. Its concrete constant-tangent semantics is \(\mathsf{Copow}(\mathbf{Vect})\), while the dependent semantics is \(\mathsf{Fam}(\mathbf{Vect})\). Since \(\mathbf{Vect}\) is Cauchy complete and direct sums provide common retract hosts, 1 gives \[\mathsf{Kar}\bigl(\mathsf{Copow}_\kappa(\mathbf{Vect})\bigr) \simeq \mathsf{Fam}_\kappa(\mathbf{Vect}).\]

References↩︎