W-types of slice polynomial functors (constructive core)

When dom = cod = I, a SlicePFunctor I I is a slice endofunctor Type/I → Type/I. Its W-type (initial algebra) is obtained as a subtype of the PFunctor W-type P.W: a tree is admitted when every node's children sit over the direction-input indices prescribed by r, and it is indexed by the q-assigned output index of its root shape.

The index (codomain-assignment) and the admissibility predicate (domain-restriction) are not written by explicit recursion. The index of a tree is the output index of its root, so it is not recursive at all; the predicate is recursive, but is obtained from mathlib's non-dependent W-type eliminator WType.elim, folding the index and the predicate together into the structure WIndex via the algebra wIndexStep. Carrying the index inside the fold is what lets the algebra state the direction-input-map condition OverInput — the children's index family, as a function of direction, equals rCurried a, the shape of SliceDomPFunctor.Compatible: the plain Prop-valued fold discards the children, so the condition would be inexpressible without either this pairing or the dependent recursor.

The carrier W is the admissible trees, with structure map wIndex. Its constructor mk and destructor dest are mutually inverse (W is a fixed point of the slice endofunctor), and elim is the morphism into any slice algebra over I. Only the existence half of the initial-algebra universal property is established here — the carrier, its fixed-point structure (mk/dest), and elim with its computation rule elim_mk and over-I law comp_elim; uniqueness of elim is not formalized. The value of elim is computed by a single non-dependent WType.elim (the fold elimData, with algebra elimStep) into the carrier ElimData — each subtree's index, its admissibility, and (given admissibility) its image value with the witness that the value lies over the index, i.e. a slice morphism (valid, const index) → (Y, p); carrying the value in the fold keeps elim's computational layer independent of the dependent recursor: elim uses WType.rec only in the proof elimData_valid, relating the fold's admissibility component to WValid. A direct WType.rec definition of a Type-valued datum (such as elim's value) would be noncomputable — the code generator does not compile recursor applications — which the project's constructive discipline forbids; a Prop-valued recursor definition such as RecProp is exempt, its content being erased. All of this stays Classical.choice-free.

The single index type is forced: the constraint compares a child's codomain-index against the parent's domain-index, so it typechecks only when dom = cod. That is the endofunctor condition an initial algebra requires.

Main definitions

SlicePFunctor.wIndexRoot — the index of a slice W-tree: the output index of its root shape. Not recursive.

SlicePFunctor.WIndex / SlicePFunctor.wIndexStep / SlicePFunctor.wIndexValid — the index-and-admissibility carrier, the algebra computing it, and the fold. SlicePFunctor.ForAll / SlicePFunctor.AllValid / SlicePFunctor.OverInput / SlicePFunctor.NodeValid are the direction-quantifier, the all-children-admissible condition (ForAll of the children's valid), the direction-input-map condition, and the node-admissibility predicate combining the latter two.

SlicePFunctor.WValid — the domain-restriction predicate: the admissibility component of wIndexValid.

SlicePFunctor.W — the carrier of the slice W-type: the admissible trees.

SlicePFunctor.wIndex — the slice W-type's structure map into I.

SlicePFunctor.W.mk / SlicePFunctor.W.dest — the constructor and destructor of the slice W-type.

SlicePFunctor.W.ElimData / SlicePFunctor.W.elimStep / SlicePFunctor.W.elimData — the elim carrier, algebra, and fold.

SlicePFunctor.W.elim — the morphism from the slice W-type into any slice algebra over I.

SlicePFunctor.W.RecProp — the paramorphism from the slice W-type into Prop: a predicate whose step sees each node and its child subtrees together with the children's predicate values.

Main statements

SlicePFunctor.wIndexValid_index_eq_wIndexRoot — the index component of the fold agrees with the non-recursive root index; one non-recursive case split.

SlicePFunctor.wValid_mk — admissibility unfolded one level.

SlicePFunctor.W.dest_mk / SlicePFunctor.W.mk_dest — mk and dest are mutually inverse.

SlicePFunctor.W.wIndex_mk / SlicePFunctor.W.comp_elim — mk and elim lie over I.

SlicePFunctor.W.elim_mk — the computation rule for elim: it is a morphism of slice algebras.

SlicePFunctor.W.elimData_valid — the fold's admissibility component agrees with WValid; a use of the dependent recursor WType.rec.

SlicePFunctor.W.induction — structural induction for the slice W-type, the wrapped form of WType.rec on the admissibility subtype.

SlicePFunctor.W.recProp_mk — the one-level computation rule for RecProp.

Implementation notes

wIndexValid folds into the structure WIndex (index, valid) via wIndexStep; a node's valid is NodeValid — AllValid (every child admissible) and OverInput (the children's index family equal to rCurried a, the Compatible shape). Its index component is the depth-1 root output index, so wIndexValid_index_eq_wIndexRoot needs only cases. elim's value is computed by elimData, a single non-dependent WType.elim with algebra elimStep into the structure ElimData (extending WIndex with a value function and an over law, a slice morphism); within elim's construction the dependent recursor is used only in the proof elimData_valid (a WType.rec application showing the fold's admissibility component agrees with WValid). A direct WType.rec definition of a Type-valued datum (such as elim's value) would be rejected by the code generator as noncomputable; a WType.rec application in a proof, or a Prop-valued WType.rec definition such as RecProp, is unproblematic. wIndexRoot, ForAll, AllValid, OverInput, NodeValid, wIndexStep, wIndexValid, WValid, W, wIndex, W.mk, W.dest, W.elimStep, W.elimData, W.elim, and W.RecProp are @[expose] so a wrapper module and the tests can unfold them across the module boundary.

References

[GambinoHyland2004]

[GambinoKock2013]

Tags

W-type, initial algebra, polynomial functor, dependent polynomial functor, slice category, container, PFunctor

The index of a slice W-tree: the q-assigned output index of its root shape. Not recursive — it reads only the root node, via PFunctor.W.head.

The index and admissibility of a slice W-tree, the two components folded together by wIndexValid.

The tree's index: the output index of its root shape.

The tree's admissibility.

Every direction satisfies the predicate P. Parallels OverInput, over F.B a.

Every child of c is admissible: ForAll of the children's valid.

The direction-input-map condition on a node's children: their index family, as a function of direction, equals the direction-input map rCurried a. Point-free — the shape of SliceDomPFunctor.Compatible for the identity projection.

A node with shape a and children c is admissible when every child is admissible (AllValid) and the children's index family lies over the direction-input map (OverInput).

The algebra computing a node's index and admissibility from its children's: the index is the q-assigned output index of the shape, and the node is NodeValid.

The index paired with admissibility: the F.toPFunctor-algebra morphism into (WIndex I, wIndexStep) given by WType.elim.

The domain-restriction predicate on slice W-trees: a tree is admitted when every node's children sit over the direction-input indices prescribed by r. The admissibility component of wIndexValid.

The index component of wIndexValid agrees with the non-recursive root index. A depth-1 fact: proved by a single non-recursive case split.

Admissibility unfolded one level: WType.mk a f is admitted exactly when every child f b is admitted and the children's index family lies over the direction-input map.

The carrier of the slice W-type: the admissible PFunctor W-trees.

The slice W-type's structure map as an object of Type/I: the index of the underlying tree.

The constructor of the slice W-type: the slice endofunctor's value at (W, wIndex) maps into W. The algebra structure map.

The destructor of the slice W-type: every admissible tree decomposes as a shape together with a compatible family of admissible subtrees. Inverse to mk.

dest is a left inverse of mk.

mk is a left inverse of dest; with dest_mk, mk and dest are mutually inverse, so W is a fixed point of the slice endofunctor.

mk lies over I: its index is the output index assigned by F.obj.

The elim fold carrier: extends WIndex to a slice morphism (valid, const index) → (Y, p) — a value function defined once the subtree is admissible, together with the proof that it lies over the index.

The image value, available once the subtree is admissible.

The value lies over the index: p ∘ value is constant at index.

The slice-algebra step of the elim fold: index and admissibility (NodeValid) as for wIndexStep, and a value function that, given a node's admissibility, applies the target algebra g to the compatible family of its children's values, with over recording that the result lies over the index.

The elim fold: the F.toPFunctor-algebra morphism into (ElimData Y p, elimStep) given by WType.elim, a single non-dependent fold with no explicit recursion.

The index component of elimData is the root index.

The admissibility component of elimData, unfolded one level.

The admissibility component of elimData agrees with WValid. An inductive step: it applies the dependent recursor WType.rec (the initial algebra's induction principle, consulting the hypothesis ih), unlike the non-recursive cases/casesOn splits elsewhere. It is in a proof, where non-computability is immaterial.

The eliminator of the slice W-type: the morphism into any slice algebra (Y, p, g) over I. The existence half of initiality. The value is computed by the non-dependent fold elimData; the tree's admissibility supplies the argument to the fold's value function.

elim lies over I: composing with the target structure map recovers wIndex.

The computation rule for elim: it commutes with the constructors, i.e. it is a morphism of slice algebras.

Structural induction for the slice W-type: a predicate holds of every admissible tree once it holds of mk x whenever it holds of each child x.1.2 b. The wrapped form of the dependent recursor WType.rec on the admissibility subtype.

Paramorphism from the slice W-type into Prop: step sees the node x, hence its child subtrees x.1.2 b, together with the children's predicate values. The value is computed by WType.rec with a Prop motive, so no noncomputable flag arises. @[expose] so the presheaf layer can unfold it.