Prototype: base-cartesian presheaf polynomial endofunctors on the walking arrow are codes

Throwaway exploration, not upstream-eligible content. Every declaration here is Classical.­choice-free.

GebProto.­LargeIR.­arrowPshCodeEquiv reads one presheaf polynomial endofunctor on the walking arrow, the transcription of a slice polynomial functor, as a large inductive-recursive code on Fam(Type). This module states the general case. A presheaf polynomial endofunctor F on the walking arrow has shapes at two levels, each shape a having directions D₀ a at level 0 and D₁ a at level 1 with a restriction ρ : D₁ a → D₀ a, and a level-1 shape a₁ restricting to a level-0 shape with reindexings of directions at each level. Its value at a walking-arrow presheaf Z, read as the family (U, T), is computed by elemEquiv: an element is a shape a, a base assignment g : D₀ a → U, and an assignment w : Π d : D₁ a, T (g (ρ d)).

The reading as a code needs one condition, BaseCartesian: for every level-1 shape, the reindexing of level-0 directions from its restriction is a bijection. Then the code is

σ (Shape 0) (fun a ↦ δ (D₀ a) (fun A ↦ σ (Π d : D₁ a, A (ρ d)) (fun w ↦ ι (fibre a A w)))),

genCode, whose σ indices are the level-0 shapes and the level-1 assignments of a level-0 shape, whose δ arities are its level-0 directions, and whose ι decodes to the level-1 shapes over it with the assignments restricting to w, genFibre. genCodeEquiv is the isomorphism of the functor's output presheaf with the presheaf of the code's interpretation at the family of the input, and arrowPshBaseCartesian exhibits the transcription of a slice polynomial functor as an instance.

The condition is not an artefact. Without it a level-1 shape carries a level-0 direction not reached from its restriction, whose value under a base assignment is an element of U unconstrained by the level-0 element below, so the fibre of the output family over that element has the index type U itself as a factor. The decoding of a code mentions U only through T ∘ g, and the interpretation of every code preserves the cartesian morphisms of families, those whose decoding maps are bijections, while a functor with such a factor does not; that argument is not formalized here.

Main definitions

• Elem, elemEquiv — the value of a presheaf polynomial endofunctor on the walking arrow in dependent-type terms.

• ElemAt, objLevel — the elements over a level, and restrElem the restriction from level 1 to level 0 on them.

• BaseCartesian — the condition on reindexing at level 0.

• genFibre, genCode — the fibre type and the code.

• arrowPshBaseCartesian — the transcription of a slice polynomial functor is base-cartesian.

Main statements

• objLevel_objRestr — the restriction of the output presheaf is restrElem on elements.

• genCodeEquiv — the output presheaf of a base-cartesian functor is the presheaf of the code's interpretation.

References

• [GhaniNordvallForsbergMalatesta2015]

  Neil Ghani, Fredrik Nordvall Forsberg, Lorenzo Malatesta (2015). “Positive Inductive-Recursive Definitions”. Logical Methods in Computer Science 11(1). https://doi.org/10.2168/LMCS-11(1:13)2015.

• [Weber2007]

  Mark Weber (2007). “Familial 2-functors and parametric right adjoints”. Theory and Applications of Categories 18(22), pp. 665–732. http://www.tac.mta.ca/tac/volumes/18/22/18-22abs.html.

Tags

prototype, presheaf, walking arrow, parametric right adjoint, inductive-recursive, code, cartesian

The value in dependent-type terms

Elements by level, and the restriction