Prototype: morphisms of presheaf p.r.a. functors, and the ι generator

Throwaway exploration, not upstream-eligible content. Every declaration here is Classical.choice-free; the bundled restatement of the p.r.a. formula, which writes ⟶ between two objects of a presheaf category and so pulls in Classical.choice from mathlib, is in the sibling PresheafIRProto.Functor module.

Two developments sit here. The larger is the morphism theory: the p.r.a. formula as the equivalence F.obj Z ≃ Σ a : F.A, ArityHom F a Z (objEquivSigmaArityHom), unindexed — its j-fibred form F Z j = Σ (a : T₁ j), Hom (E a) Z is reached through ObjFib and ofSigmaFib — the morphism type PshHom with its action, and the representation theorem pshHomEquivNatFamily classifying the natural families between two such functors by shape-map-forward and arity-map-backward data, with DomHom / domHomEquivNatFamily as its domain-level warm-up. The smaller, first in the file, is the constant functor at a representable. The code type itself and its two rules are in the sibling PresheafIRProto.Codes module; nothing here is a code constructor.

Two claims are tested here:

iotaPresheaf — the constant (iota) case generalizes to the functor constant at the representable y j₀, whose shape type is the total space Σ j', (j' ⟶ j₀) of that representable rather than a single shape.

Functoriality — that IR.rec reaches the subcodes, which is all it establishes. Its witness type is built from IR.Hom, whose ι-clause is propositional equality of indices and so ignores C₀'s morphisms; it is not the type the source requires.

Main definitions

GebProto.isFunctorial_of_subsingletonDirection — the five direction-side functor laws where every direction fibre is a subsingleton.

GebProto.idPshHom — the identity morphism of presheaf p.r.a. functors.

GebProto.SliceHom / GebProto.sliceHomApp — the morphism formula at a discrete base, and its action.

GebProto.iotaPresheaf / iotaPresheafData — the constant functor at a representable, and its operations.

GebProto.Functoriality — the witness family attached over pre-codes.

GebProto.ArityB — the fibre family the worked example in Codes is built on.

GebProto.shapePresheaf / GebProto.arityPresheaf — the shape presheaf T₁ and the arity presheaf E(a), as Functor values built from the raw fields.

GebProto.ArityHom / GebProto.ofArityHomElt / GebProto.objEquivSigmaArityHom — the p.r.a. formula T Z ≃ Σ a, Hom(E(a), Z) with the presheaf hom unbundled, hence free of Classical.choice, and the slice element its inverse produces.

GebProto.DomHom / GebProto.DomNatFamily / GebProto.domHomEquivNatFamily — the domain-level morphism data, the natural families it represents, and the Yoneda equivalence between them.

GebProto.ShapeHom — the unbundled presheaf hom T₁ ⟶ T₁'.

GebProto.PshHom — the full morphism data of presheaf p.r.a. functors: a ShapeHom, a backward arity map, and the el(T₁) naturality of the latter, stated across a transport along the former's naturality.

GebProto.ObjFib / GebProto.objFibRestr / GebProto.objFibMap / GebProto.ofSigmaFib — the output presheaf's fibres, their J-restriction and input-presheaf action, unbundled, and the fibre element of a shape and an arity hom.

GebProto.pshHomFib — the action of a PshHom on those fibres.

GebProto.PshNatFamily / GebProto.pshHomEquivNatFamily — the natural families a PshHom represents, and the equivalence between them.

Main statements

GebProto.pshHomFib_objFibRestr — the action of a PshHom commutes with the J-restriction, which is the content of PshHom's reindexCompat clause.

References

[GhaniNordvallForsbergMalatesta2015]

[GhaniMalatestaNordvallForsberg2014Agda]

[HancockMcBrideGhaniMalatestaAltenkirch2013]

[Weber2007]

Tags

prototype, inductive-recursive, presheaf, parametric right adjoint

Where every direction fiber is a subsingleton, the five direction-side functor laws are all Subsingleton.elim and only the two shape-side laws carry content. iotaPresheaf is of that kind.

The operations of the constant functor at the representable y j₀: shapes are the total space of y j₀, the shape-output map is its projection, there are no directions, and shapeRestr is precomposition.

Every direction fiber of iotaPresheafData is empty, hence a subsingleton; this discharges all five direction-side functor laws.

The functor whose shape type is the total space of the representable y j₀ and which has no directions, as a PresheafPFunctor. That its shape presheaf is y j₀ is not established here. The shape-side laws are the category laws of J; the direction-side laws hold because every direction fiber is empty.

Can the functoriality witness be attached after the codes, rather than as a code field defined simultaneously with the morphisms?

That depends on which morphism collection is taken. Remark 3.4 of [GhaniNordvallForsbergMalatesta2015] states that its results are parametric in that choice: any collection representing natural transformations between the codes works, provided identities and composition are definable. Its Definition 3.1 takes a natural transformation, whose naturality refers to the witnesses and to composition of code morphisms; [GhaniMalatestaNordvallForsberg2014Agda] takes a bare family of components, whose δ→δ rule mentions the witnesses only in its conclusion's indices, never in its premises. Under the latter the morphism type does not depend on the witnesses, so the witness can be attached afterwards, by IR.rec against an already-defined morphism type.

Functoriality below demonstrates only that IR.rec reaches the subcodes, which is what such an attachment needs. Its witness type is built from IR.Hom, whose ι-clause is propositional equality of indices and so ignores the category's morphisms; that is not the type the source requires, and no claim is made here that this witness is the right one.

The functoriality witness of a code, attached after the fact by IR.rec: nothing at ι, componentwise at σ, and at δ the Positive-IR witness F→ — a code morphism between the subcodes at any two labellings related by a family of C₀-morphisms — paired with the witnesses of those subcodes.

That this elaborates at all is the point: IR.Hom is already defined, so the witness needs no mutual definition with the codes.

reindex is the obligation neither prior paper has an analogue for: Positive IR's F→ witnesses functoriality of subcodes in the input labelling (A → C), which is the directionRestr side, whereas reindex witnesses functoriality of the arity assignment over el(T₁) — the output side.

ArityB below is the fibre family the worked example in Codes is built on: one direction at 1, none at 0, so that reindexing along 0 ⟶ 1 is the map out of the empty type.

The arity of the output object a: one direction at 1, none at 0. Codes' arityVariesBase takes its fibres from this.

Each fibre of ArityB is a subsingleton: Fin 0 is empty and Fin 1 is a point, so the two elements of any fibre are equal.

The regular formula for natural transformations between polynomial functors: shapes forward, arities backward. For slice polynomial functors F, F' over the same dom and cod, a transformation is a map of shapes over each output index together with, for each shape, a map of arities in the opposite direction. SliceHom carries no naturality field; sliceHomApp below constructs the action from those two components alone.

Derivation, for the presheaf case: T Z j = Σ_{a ∈ T₁ j} Hom(E a, Z) is a coproduct of representables in Z, so by Yoneda Nat(Σ_a Hom(E a, −), Σ_b Hom(E' b, −)) = Π_a Σ_b Hom(E' b, E a). Yoneda for covariant hom-functors holds in any locally small category, so it is not what restricts the argument. What restricts it is the premise: over the free coproduct completion the δ interpretation is not a coproduct of Fam(C)-representables, since by Theorem 2.4 of [GhaniNordvallForsbergMalatesta2015] its coproduct is indexed by set maps A → X, whereas by Definition 2.2 a Fam(C)-morphism carries C-morphism data that index does not.

A morphism of slice polynomial functors: shapes forward over each output index, arities backward at each shape. This is Definition 7 of [HancockMcBrideGhaniMalatestaAltenkirch2013] (morphisms of indexed containers) at a discrete base.

The shape map, over each output index.

The arity map, in the opposite direction, at each shape and base point.

The action of a SliceHom on the domain-restricted functor's value: the shape travels forward, and each direction of the new shape is filled by pulling it back along arity and reading off the original assignment. That this is definable with no further data is the content of the formula.

The two presheaves the p.r.a. formula names, extracted from the raw fields as Functor values, on the model of PresheafPFunctor.objPresheaf.

shapePresheaf lands in Type uA and arityPresheaf in Type uB, those being the universes of SlicePFunctor.Shape (a Subtype of F.A : Type uA) and of SliceDomPFunctor.Direction (a Subtype of F.B a : Type uB). Neither carries a max with the base or morphism universes: Shape j is cut out of F.A by a Prop, and Direction a i out of F.B a by a Prop.

Consequently arityPresheaf F a : Iᵒᵖ ⥤ Type uB is an object of the same category as Z : Iᵒᵖ ⥤ Type uZ only when uB and uZ are the same level. Lean's Type hierarchy is not cumulative, so no relation uB ≤ uZ (which is not expressible on levels anyway) helps; the two options are to instantiate uZ := uB, or to ULift both sides into Type (max uB uZ). Both are exhibited below.

The shape presheaf T₁ : Jᵒᵖ ⥤ Type uA of the familial presentation of [Weber2007]: fibre F.Shape j over j, restriction maps F.shapeRestr, functor laws from shapeRestr_id / shapeRestr_comp.

The arity presheaf E(a) : Iᵒᵖ ⥤ Type uB of a shape a, the second half of [Weber2007]'s familial presentation: fibre F.Direction a i over i, restriction maps F.directionRestr a, functor laws from directionRestr_id / directionRestr_comp.