W-types of presheaf polynomial functors: hereditary naturality (constructive core)

For a presheaf polynomial endofunctor F : PresheafPFunctor I I, the W-type of the underlying slice endofunctor F.toSlicePFunctor : SlicePFunctor I I carries a tree-level naturality predicate. A slice W-tree assembles a shape with a compatible family of child subtrees; the presheaf structure additionally acts on directions contravariantly (directionRestr) and on the assignment of shapes to output indices. A tree is hereditarily natural when, at every node, restricting a child subtree along a morphism agrees with selecting the child at the reindexed direction, hereditarily through the whole tree.

wRestrTree is the root-only restriction of a slice W-tree along a morphism: it restricts the root shape and reindexes the direction-assignment via the generalized PresheafPFunctor.objRestrElt, conjugated by the slice destructor and constructor. IsHereditarilyNatural folds the local naturality equation over the whole tree through the slice W-type's Prop-valued paramorphism SlicePFunctor.W.RecProp; isHereditarilyNatural_mk is its one-level computation rule.

Main definitions

PresheafPFunctor.wRestrTree — the root-only restriction of a slice W-tree along a morphism, via the generalized objRestrElt at p := wIndex.

PresheafPFunctor.IsHereditarilyNatural — the tree-level naturality predicate on slice W-trees, defined by SlicePFunctor.W.RecProp.

PresheafPFunctor.wRestr — restriction on the ULifted carrier fiber, reindexing the underlying tree along a morphism while preserving the index and hereditary naturality.

PresheafPFunctor.W — the carrier presheaf Iᵒᵖ ⥤ Type (max uI uA uB), whose fiber over j is the ULift of the hereditarily-natural slice W-trees indexed at j and whose restriction maps are wRestr.

PresheafPFunctor.W.forgetNode / PresheafPFunctor.W.rememberNode — the mutually inverse translations between a presheaf node over the carrier presheaf F.W and the underlying slice node over wIndex together with the hereditary naturality of its children.

PresheafPFunctor.W.mk / PresheafPFunctor.W.dest — the fixed-point constructor and destructor: mutually inverse fiberwise maps between the objPresheaf-value at F.W and F.W, exhibiting F.W as a fixed point of the objPresheaf-action at F.W.

PresheafPFunctor.W.PElimData / pElimStep / pElimData — the eliminator's fold carrier, algebra, and fold (a WType.elim fold whose value is guarded by hereditary naturality, since the presheaf algebra acts only on natural nodes): the presheaf analogue of the slice ElimData machinery.

PresheafPFunctor.W.elimVal — the eliminator's value on a carrier element, extracted from the fold given the tree's hereditary naturality.

PresheafPFunctor.W.elim — the eliminator into any presheaf algebra (Y, α), a natural transformation F.W ⟶ Y.

PresheafPFunctor.MemW — membership of a raw W-tree in the carrier presheaf's fiber over an index, stated on F.toPFunctor.W so that it can be decided by a fold.

Main statements

PresheafPFunctor.isHereditarilyNatural_mk — the one-level unfolding of IsHereditarilyNatural on a constructor SlicePFunctor.W.mk x: local naturality at the root, together with hereditary naturality of every child.

PresheafPFunctor.wIndex_wRestrTree — the index of a root-restricted tree is the restriction morphism's source.

PresheafPFunctor.isHereditarilyNatural_wRestrTree — hereditary naturality is preserved by the root-only restriction, a one-level argument.

PresheafPFunctor.wRestrTree_id / PresheafPFunctor.wRestrTree_comp — the functoriality of wRestrTree, from which W's functor laws transport.

PresheafPFunctor.W.dest_mk / PresheafPFunctor.W.mk_dest — mk and dest are mutually inverse, so F.W is a fixed point of the objPresheaf-action at F.W.

PresheafPFunctor.W.isHereditarilyNatural_mk_forgetNode — hereditary naturality of the slice tree built from a presheaf node over F.W is exactly the node's IsNatural datum; the correspondence underlying mk / dest and the eliminator fold.

PresheafPFunctor.W.comp_elim — elim is a morphism of presheaves (its NatTrans naturality), from elimVal_wRestr.

PresheafPFunctor.W.elim_mk — the computation rule: elim commutes with mk, i.e. it is a morphism of presheaf algebras.

PresheafPFunctor.memW_iff_exists_obj — MemW holds exactly of the trees underlying the carrier presheaf's fiber.

Implementation notes

This is the presheaf endofunctor case, I = J, so the slice endofunctor F.toSlicePFunctor : SlicePFunctor I I has a W-type. wRestrTree and IsHereditarilyNatural act on the un-lifted trees F.toSlicePFunctor.W of type Type (max uA uB); the carrier presheaf W ULifts the indexed subtype into Type (max uI uA uB) so its fibers land in a single universe with the index category I.

The recursion in IsHereditarilyNatural is confined to the slice W-type's Prop-valued paramorphism SlicePFunctor.W.RecProp: no explicit self-recursion and no induction tactic appear. The child-index witness required by wRestrTree is discharged from the compatibility of the node's direction-assignment (SliceDomPFunctor.compatible_iff) together with the direction's fiber constraint, exactly as PresheafDomPFunctorData.value obtains its index equality.

The eliminator elim folds the underlying slice tree into a target value with a bespoke WType.elim fold (pElimData, carrier PElimData, algebra pElimStep), the presheaf analogue of the slice elim's ElimData fold. The presheaf algebra α acts only on natural nodes, so — unlike the slice elim, whose algebra is total — the fold's value is a function of the subtree's hereditary naturality, and the fold carries a naturality proxy (via the guard P ∧ ∀ hp : P, Q hp, the standard And with Q proof-irrelevant in hp) letting α apply at each node. The value fold is a non-dependent WType.elim (code-generatable); the recursion in the accompanying proofs (pElimData_valid, elimVal_wRestr) stays inside WType.rec / SlicePFunctor.W.induction. Only the existence half of the initial-algebra universal property is established — the carrier, its fixed-point structure, and elim with its computation rule elim_mk and naturality law comp_elim; uniqueness of elim is not formalized.

References

[Weber2007]

[GambinoHyland2004]

[GambinoKock2013]

[AltenkirchGhaniHancockMcBrideMorris2015]

Tags

W-type, initial algebra, polynomial functor, presheaf, parametric right adjoint, naturality, restriction map, PFunctor

The root-only restriction of a slice W-tree z along a morphism g : j' ⟶ j (where j is the index of z): restrict the root shape and reindex its direction-assignment via the generalized objRestrElt at the projection p := F.toSlicePFunctor.wIndex, conjugating by the slice destructor and constructor. The head-index witness required by objRestrElt is the hypothesis hq, the root's q-output index being read from PFunctor.W.head.

Hereditary naturality of a slice W-tree: at every node, restricting a child subtree along a morphism g agrees with selecting the child at the reindexed direction, hereditarily. The local conjunct is the tree analogue of PresheafDomPFunctorData.IsNatural; the fold over the tree is carried by the slice W-type's Prop-valued paramorphism SlicePFunctor.W.RecProp.

One-level unfolding of IsHereditarilyNatural on a constructor SlicePFunctor.W.mk x: local naturality at the root together with hereditary naturality of every child subtree. From SlicePFunctor.W.recProp_mk.

The index of a root-restricted tree is j': wRestrTree g z rebuilds the root with the restricted shape (shapeRestr g _).1, whose q-output index is j'.

The child a root-restricted node assigns to a direction is the child the original node assigns to the direction's reindex. The analogue of value_objRestrElt for the raw child assignment; rfl after destructuring the direction, matching objRestrElt's internal ⟨·, rfl⟩ reconstruction.

Hereditary naturality is preserved by the root-only restriction: the children of wRestrTree g z are the original subtrees reindexed (each already hereditarily natural), and its root's local naturality follows from z's own root local naturality and reindex_naturality. A one-level argument, not a recursion.