ch:containers-ornaments: ch:containers-ornaments

The unique shape is $\star :\mathbf{1}$ and the contents function $f:\mathsf{Fin}(2)\to X$ is $f(0)=a$ and $f(1)=b$. Hence the element is $(\star ,[a,b])$. Container action leaves the shape fixed: $${\mathsf{cmap}}_{C_{\mathsf{Bin}}}(h,(\star ,[a,b]))=(\star ,[h(a),h(b)]).$$ This is one binary-node layer: its contents label two recursive positions. A complete tree arises only after taking an appropriate fixed point of the layer operator.

Let $m_S(n)=n\mathsf{-}1$ and $m_P(n,i)=\mathsf{suc}(i)$. If $i:\mathsf{Fin}(n\mathsf{-}1)$, then $\mathsf{suc}(i):\mathsf{Fin}(n)$. At shape $0$ the target has shape $0$ and no positions. At shape $3$, $$⟨m{⟩}_X((3,[x_0,x_1,x_2]))=(2,[x_1,x_2]).$$ A nonempty target at source shape $0$ would require a function from some inhabited target-position type to $\mathsf{Fin}(0)$, which is impossible.

Represent $F$ by the sum of the zero-position unit container and the one-position container with shape $A$; represent $G$ by one shape with two positions. Composition gives $F\circ G$ either zero positions or two positions indexed by a chosen $a:A$. Product gives $G\circ F$ a pair of $F$-shapes and therefore $0$, $1$, or $2$ positions. In particular the shape $(\mathsf{nilShape},\mathsf{consShape}(a))$ of $G\circ F$ has one position, whereas no shape of $F\circ G$ does. Thus the two polynomial operators are not identified by reassociation.

Set For $u=(a,h)$ in the successor fiber, its unique recursive child is $h(\star ):X(k)$. Replacing the last equation by $n(\mathsf{suc}(k),a,\star )=\mathsf{suc}(k)$ makes the child have type $X(\mathsf{suc}(k))$. The recursive index no longer descends from the result index, so the layer no longer describes the vector constructor.

The derivative is $$\partial (A+X\times X)=0+(1\times X+X\times 1)\simeq X+X.$$ For $\mathsf{fork}(l,r)$ the left-hole context stores $\mathsf{inl}(r)$ and plugs $x$ as $\mathsf{fork}(x,r)$; the right-hole context stores $\mathsf{inr}(l)$ and plugs $x$ as $\mathsf{fork}(l,x)$. These are the two summands of the product rule, each storing the sibling belonging to the undifferentiated factor.

The result has type $\mathsf{Vec}(A,m+n)$. Induct on $xs$. At $\mathsf{vnil}$ both sides compute to $\mathsf{forget}(ys)$. At $\mathsf{vcons}(a,zs)$, both sides expose the head $a$ and the induction hypothesis identifies their tails: The forgetful map erases the result index $m+n$ while retaining the list spine.

A binary-node layer has two recursive positions. A leaf layer has none. A forgetful morphism from the alleged refinement back to the binary layer would need a position map from each of those two target positions to a position of the leaf source. Its codomain is empty, so no such function exists. For a family map that distinguishes the missing right child, the induced map to the pullback is not surjective and hence is not an equivalence. Thus the proposal violates the cartesian clause of definition 81.16; selecting only the left child does not repair the missing right position.

Induct on the relation witness. At $0$ the input list is nil, list map is nil, and ${\mathcal{R}}_B(0,\mathsf{nil})$ is immediate. At a successor, write $xs=\mathsf{cons}(a,zs)$. The induction hypothesis gives ${\mathcal{R}}_B(n,\mathsf{mapList}(f,zs))$; the successor/cons clause yields $${\mathcal{R}}_B(\mathsf{suc}(n),\mathsf{cons}(f(a),\mathsf{mapList}(f,zs))).$$ The ML type is (’a -> ’b) -> ’a list -> ’b list. It does not state that the output length equals the input length; that fact remains the displayed logical relation.

Reverse has shape component $n\mapsto n$ and position component $r_n(i)=n-1-i$. Its self-composite has shape component the identity and position component $$i⟼r_n(r_n(i))=n-1-(n-1-i)=i(i:\mathsf{Fin}(n)).$$ Hence for every $(n,f)$ its extension is $(n,\lambda i.f(i))$, pointwise equal to $(n,f)$.

Write $L=1+A\times X$ and $R=1+B\times X$. The product rule gives $$\partial (L\times R)\simeq (A\times R)+(L\times B).$$ An element $\mathsf{inl}(a,r)$ is a hole in the $L$ recursive position and plugs $x$ as $(\mathsf{inr}(a,x),r)$. An element $\mathsf{inr}(l,b)$ is a hole in the $R$ recursive position and plugs $x$ as $(l,\mathsf{inr}(b,x))$. For example, $\mathsf{inl}(a,\mathsf{inl}\star )$ and $\mathsf{inr}(\mathsf{inr}(a,x_0),b)$ inhabit the two summands.

Take $A=\mathbf{1}$. Finite lists form the initial algebra of $F(X)=1+\mathbf{1}\times X$. The type containing one finite list for each natural length together with one infinite stream is also closed under the same one-step equation: the extra element is sent to the successor branch with itself as tail. Thus a bare fixed-point equivalence does not choose between them. Initiality distinguishes finite lists by the unique algebra morphism out; finality distinguishes the possibly infinite solution by the unique coalgebra morphism in.