Prototype: the parts that write in a functor category

Collects what the choice-free core (PresheafIRProto.Basic, PresheafIRProto.Codes) cannot state. Writing ⟶ between two objects of a presheaf category, or ⥤ into one, invokes CategoryTheory.Functor.category, which is Classical.choice-dependent, so every declaration needing either lives here and this module alone is on GebMeta.classicalAllowedModules.

Five things sit here. The p.r.a. formula T Z ≃ Σ a, Hom(E(a), Z) with its hom written as arityPresheaf F a ⟶ Z, obtained by transporting the core's GebProto.objEquivSigmaArityHom along the bundling isomorphism arityHomEquivNatTrans — a CategoryTheory.NatTrans is its app field together with naturality, and GebProto.ArityHom is that data unbundled, so the isomorphism is the identity on both sides and no part of the formula is re-proved. The two universe-formability demonstrations recording where the bundled hom is formable. And BaseArity.functor, the output-indexed arity bundled as a functor into the presheaf category, whose two functor laws are proved here rather than transported.

Main definitions

GebProto.arityHomEquivNatTrans — the bundling isomorphism between the unbundled arity hom and the functor-category hom.

GebProto.objEquivSigmaHom — the p.r.a. formula of [Weber2007] with the presheaf hom bundled.

GebProto.arityPresheafHomAtUB / GebProto.arityPresheafHomULifted — the universes at which the bundled hom is formable.

GebProto.BaseArity.functor — an output-indexed arity as a functor J ⥤ (Iᵒᵖ ⥤ Type uB), the output base to discrete fibrations over the input base.

References

[Weber2007]

Tags

prototype, presheaf, parametric right adjoint, functor category

The bundling isomorphism: an unbundled arity hom is a natural transformation E(a) ⟶ Z. Forward is natTransOfArityHom, backward reads off the components and re-states naturality elementwise; both round trips are definitional.

The p.r.a. formula: the domain-restricted interpretation of F at Z is the coproduct over shapes of the representables on the arity presheaves. The core objEquivSigmaArityHom transported fibrewise along the bundling isomorphism.

At uZ := uB the arity presheaf and the input presheaf are objects of one category, so the hom the p.r.a. formula needs is formable with no transport.

At an unrelated uZ the hom is formable after ULifting both sides into Type (max uB uZ); max is commutative on levels, so the two composites are objects of one category.

A functorial BaseArity is a functor from the output base to presheaves on the input base — equivalently, to discrete fibrations over it. This is the δ rule's arity datum in bundled form: famPresheaf is the object part, reindexHom the morphism part, and the remaining two clauses of BaseArity.IsFunctorial are the functor laws.

Kept here rather than in the choice-free core because the target Iᵒᵖ ⥤ Type uB is a functor category, whose Category instance is Classical.choice-dependent.