Prototype: the walking arrow over an index type

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

A presheaf polynomial endofunctor on the walking arrow acts on Fam(Type), where the base of a family is data, and its directions can name an element of the base only through a function from a fixed set, so a slice polynomial functor transcribed to it is recovered only up to a section and its W-type is not recovered at all. On the discrete category of an index type X, presheaves are Type/X, a direction names its index exactly, and the presheaf polynomial functors are the slice polynomials with their W-types. This module takes the product of the two: the category Idx X, the pairs (i, x) of a level and an index ordered by i ≤ i' and x = x', whose presheaves are X-indexed families of arrows, the objects (U : X → Type, T : Π x, U x → Type) of indexed induction-recursion. A direction at (j, x) names its index x by its object, and only an element of U x through a function.

elemEquiv computes the value of any presheaf polynomial endofunctor on Idx X: a shape, a base assignment at each index, and an assignment of level-1 directions in the fibres over it, the naturality along the one non-identity morphism at each index being the fibre condition, isNatural_iff. prodPsh transcribes a slice polynomial functor P : Type/X → Type/Y: level-0 shapes Y with no directions, so that the base is constantly a point, and level-1 shapes the shapes of P, each direction b of P giving a level-1 direction at (1, r b) with its restriction at (0, r b). ofSliceX embeds Type/X as the presheaves with a point at every level 0, and levelOneEquiv identifies the level-1 value of the transcription at ofSliceX p over (1, y) with the value of P at p over y, on the nose; map_cmp extends this to morphisms over X. For an endofunctor, wFixed then exhibits the slice W-type SlicePFunctor.­W as a fixed point of the transcription: the iteration of the transcription on the initial object of Type/X, which stays over the constant point, is the iteration of P.

Main definitions

• Idx — the walking arrow over an index type, as a preorder.

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

• prodPsh — the transcription of a slice polynomial functor.

• ofSliceX, ofSliceXHom — Type/X as presheaves on Idx X.

• levelOneEquiv, cmp — the level-1 value at an object of Type/X is the slice functor's value, and the comparison map.

• wFixed — the slice W-type is a fixed point of the transcription.

Main statements

• isNatural_iff — naturality over Idx X is the fibre condition at each index.

• levelZeroEquiv — the transcription's base is a point at every index.

• map_cmp — the comparison map is natural in the object of Type/X.

References

• [DybjerSetzer2003]

  Peter Dybjer, Anton Setzer (2003). “Induction--recursion and initial algebras”. Annals of Pure and Applied Logic 124(1--3), pp. 1–47. https://doi.org/10.1016/S0168-0072(02)00096-9.

• [HancockMcBrideGhaniMalatestaAltenkirch2013]

  Peter Hancock, Conor McBride, Neil Ghani, Lorenzo Malatesta, Thorsten Altenkirch (2013). “Small Induction Recursion”. Typed Lambda Calculi and Applications (TLCA 2013) 7941, pp. 156–172. https://doi.org/10.1007/978-3-642-38946-7_13. This repository cites the TLCA 2013 proceedings numbering (Definition 8, Theorems 2/3/4, Corollary 2). The extended 2012 preprint at https://personal.cis.strath.ac.uk/conor.mcbride/pub/SmallIR/SmallIR.pdf renumbers two of these: its Theorem 15 is the proceedings' Theorem 2, and its Theorem 21 is the proceedings' Theorem 4..

Tags

prototype, presheaf, walking arrow, indexed inductive-recursive, slice polynomial functor, W-type

The index category

The value of an endofunctor