Prototype: code combinators at the presheaf p.r.a. level

Throwaway exploration, not upstream-eligible content. Continues PresheafIRProto.Basic with the semantic counterparts of the code constructors of Section 6 of [HancockMcBrideGhaniMalatestaAltenkirch2013], generalized from families to presheaves. Basic supplies iotaPresheaf; this module supplies the semantic operations and the code type.

Main definitions

GebProto.DomArity — a presheaf on I unbundled, in the presentation PresheafDomPFunctorData uses for its arities.

GebProto.ShapeArity — the arity a δ adjoins, varying over the shape presheaf.

GebProto.adjoinArityData / GebProto.adjoinArity — δ's direction-adjoining half, which is not δ: adjoin a ShapeArity to every arity of a functor, leaving the shapes untouched.

GebProto.BaseArity / GebProto.BaseArity.pullback — the arity a code's δ carries, indexed by output objects rather than by shapes, and its pullback along a functor's shape-output map to the ShapeArity that adjoinArity consumes.

GebProto.ElObj / GebProto.elCategory — the category of elements of a presheaf on J, as a base category. Presheaves on it are expected to be the slice PSh(J)/S; nothing here establishes that.

GebProto.sigmaLiftHom / GebProto.sigmaPshData / GebProto.sigmaPsh — the σ case: push a functor over the base ElObj S forward along the projection to J.

GebProto.elEqToHom — the transport in the category of elements, with its underlying J-morphism definitionally an eqToHom.

GebProto.PshMor — a morphism from a DomArity to a presheaf, unbundled: the decodings a δ's continuation may depend on.

GebProto.fibreArity — the arity a decoding adjoins, its fibres.

GebProto.decPresheaf / GebProto.decArity / GebProto.delta — the decodings of an output-varying arity as a presheaf on the output base, the arity indexed by that presheaf's elements, and the δ carrying both features.

GebProto.CodeShape / GebProto.CodeDir / GebProto.CodeNext / GebProto.codePFunctor — the polynomial functor on Cat whose W-type is the type of codes, and GebProto.Code, that W-type.

GebProto.praCode / GebProto.deltaCode — the two code constructors. pra abbreviates parametric right adjoint: the leaf injects a presheaf p.r.a. functor as it stands, and δ adjoins an arity with one continuation over the category of elements of its decoding presheaf.

GebProto.Interp — the interpretation's target, a presheaf p.r.a. functor paired with the base category it lands in.

GebProto.DomArity.presheaf — an arity's fibrewise presentation, as a presheaf on the input base.

GebProto.BaseArity.famPresheaf / GebProto.BaseArity.reindexHom — an output-indexed arity's presheaf at each output object, and the morphism of presheaves each output morphism induces.

GebProto.termPsh / GebProto.arityVariesBase / GebProto.deltaVaries — the worked example's decoding target, its output-varying arity, and the δ at it.

GebProto.deltaCodeVaries — a δ code at that arity.

GebProto.codeAlgOn / GebProto.codeAlg / GebProto.interp — the interpretation of a code node, the slice algebra it assembles into, and the fold.

GebProto.praCodeOf — the leaf as a section of the interpretation.

Main statements

GebProto.BaseArity.isFunctorial_pullback — the pullback of a functorial BaseArity is functorial, so a code's δ need not mention its subcode's shapes.

GebProto.sigmaPsh_shapeRestr_id, GebProto.sigmaPsh_shapeRestr_comp, GebProto.sigmaPsh_reindex_naturality, GebProto.sigmaPsh_reindex_id, GebProto.sigmaPsh_reindex_comp — the five laws the σ case does not inherit unchanged from its subfunctor.

GebProto.elObj_eq_of_hom / GebProto.elHom_eq_eqToHom_comp — the source of a morphism of elements is determined by its base and its underlying J-morphism, and two morphisms with equal underlying J-morphisms differ by that transport.

GebProto.interp_praCode, GebProto.interp_deltaCode — the interpretation's computation rules, one per constructor, each definitional. The first of them is what makes the interpretation surjective on objects.

GebProto.interp_praCode_interp — every code has the interpretation of a one-node code, so δ adds no functor the leaf does not already supply.

GebProto.leftInverse_interp_praCodeOf, GebProto.surjective_interp — the interpretation retracts onto the leaf, so the codes denote exactly the presheaf p.r.a. functors over ElObj D at the universes CodeShape pins.

GebProto.interp_deltaCodeVaries — the check that interp_deltaCode's transports reduce at a closed instance.

GebProto.interp_fst — a code's index is the base its interpretation lands in.

Implementation notes

ShapeArity indexes the adjoined arity by F's shapes rather than by output objects, which is what keeps adjoinArityData free of transports: the arity of the shape a is fam a, not fam (F.q a) transported along a's membership proof. Its IsFunctorial mirrors PresheafPFunctorData.IsFunctorial clause for clause, so adjoinArity's law proofs split over the two direction summands into the arity's law and F's.

BaseArity.pullback is where the transport ShapeArity avoids reappears: its reindexing runs along g conjugated by the two shape-membership proofs, so its two transported laws reduce to equalities of J-morphisms built from eqToHoms. BaseArity.reindex_eqToHom, BaseArity.reindex_cast_shape and BaseArity.reindex_comp_apply are the three lemmas that reduction needs.

The σ case's laws are eqToHom bookkeeping over ElObj S. Two devices carry them. elEqToHom is a transport whose underlying J-morphism reduces definitionally, because eqToHom is opaque to rw and simp and blocks the J-level identities the laws reduce to. And the reindexing laws are stated and combined through HEq, because a direction over a restricted shape and its counterpart over the same shape reached by a different route have types that agree only once the morphisms are identified; reindex_heq_congr_shape, reindex_heq_eqToHom, reindex_eq_of_eq_comp and reindex_eq_of_eq_eqToHom_comp are the resulting toolkit.

The code type is the W-type of a slice polynomial functor on Cat, not an inductive family: the index is a base category, which δ replaces by the category of elements of its decoding presheaf. Cat.{v, u} is closed under that step because the category of elements of a presheaf valued in Type u on a base in Type u is again in Type u, with homs a subtype of the base's. The arity carrier universe is pinned to the base's, which the prototype does not need to vary. Nothing here is defined simultaneously with anything else, so no inductive-inductive definition or encoding of one is required.

References

[DybjerSetzer1999]

[HancockMcBrideGhaniMalatestaAltenkirch2013]

[MacLaneMoerdijk1992]

[nLabParametricRightAdjoint]

Tags

prototype, inductive-recursive, presheaf, parametric right adjoint

A presheaf on I, unbundled: a carrier with a base-point map proj, the directions over i being the fiber of proj, and the contravariant action restr on those fibers. Presented the way PresheafDomPFunctorData presents its arities, so that these directions plug into a PresheafPFunctorData's without transport.

Writing this as Iᵒᵖ ⥤ Type uB and its morphisms with ⟶ would draw in Classical.choice through CategoryTheory.Functor.category.

The total space of the arity.

The base-point map assigning each element of the carrier an input object.

The contravariant I-action on the fibers of proj.

The directions lying over the input object i: the fiber of proj.

The presheaf laws of a DomArity.

restr preserves identities.

restr reverses composition.

The arity as a presheaf on the input base: the fibers of proj with their own restriction. A DomArity is the total-space presentation of a discrete fibration over I, and this is the presheaf that fibration classifies. Discrete fibrations in this role are what [nLabParametricRightAdjoint] specifies.

The arity adjoined by a δ, varying over F's shape presheaf: a presheaf on I for each shape, together with a reindexing along shape restriction. This carries a family over F.A with a reindexing along shapeRestr; reading that as the unbundled data of a functor el(T₁) ⥤ (Iᵒᵖ ⥤ Type) — covariant, since a morphism of el(T₁) runs from a restricted shape to the shape and reindex follows it — is not elaborated here, there being no counterpart of BaseArity.functor for it — the same data PresheafPFunctorData carries in its directionRestr and reindex fields.

Indexing by shapes rather than by output objects is what keeps the δ operation transport-free: the arity of the shape a is fam a, not fam (F.q a) transported along a's membership proof.

The presheaf on I adjoined over each shape.

Reindexing along shape restriction, in the direction of PresheafPFunctorData.reindex.

The functor laws of a ShapeArity, mirroring those of PresheafPFunctorData clause for clause: reindex_id and reindex_comp carry the same cast along F's shape-restriction laws.

Each adjoined presheaf preserves identities.

Each adjoined presheaf reverses composition.

Reindexing is a morphism of presheaves on I.

Reindexing along an identity is the transport along F.shapeRestr_id.

Reindexing along a composite factors, modulo the transport along F.shapeRestr_comp.

Operations of δ's direction-adjoining half: adjoin the arity P to every arity of F, leaving the shapes untouched.

Transport of an adjoined direction along an equality of shapes is the transport of that direction inside the arity.

Transport of an original direction along an equality of shapes is the transport of that direction inside F.

Adjoining an arity to a presheaf p.r.a. functor yields one: the shape-side laws are F's unchanged, and each direction-side law splits over the two summands into the arity's law and F's.

This is not δ. It is δ's direction-adjoining half; delta is the rule, and adds the coproduct over decodings that this leaves out.