Prototype: the transcription and the code agree on morphisms

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

GebProto.­LargeIR.­arrowPshCodeEquiv identifies the output presheaf of the transcription GebProto.­LargeIR.­arrowPsh of a slice polynomial functor P at a walking-arrow presheaf Z with the presheaf of the interpretation of the code GebProto.­LargeIR.­code at the family of Z. This module extends the agreement to morphisms. The morphisms of Fam(Type) proper, FamHom, are a map of index types with a map of decodings over it, the morphisms of the Grothendieck construction of U ↦ (U → Type), in contrast to those of CategoryTheory.­FreeCoprodCompDisc, which compare decodings by equality. On them the code acts by codeMap: the σ index and the ι point are fixed, the δ assignment is postcomposed with the map of index types, and the decoding is carried along by the functoriality fibreValueMap of the slice functor's fibre in the family, which is the positivity of the code's continuation in the sense of

A morphism of walking-arrow presheaves is a morphism of families, famHomOfNatTrans, and conversely, natTransOfFamHom, through the presheaf morphism arrowHom of a commuting square over a base change. The naturality statements base_map and total_map say that GebProto.­LargeIR.­arrowPshCodeEquiv commutes with the transcription's action PresheafPFunctor.­mapPresheaf on one side and codeMap on the other: the isomorphism is natural in the input presheaf, so the transcription and the positive action of the code are the same functor on Fam(Type) up to it. Both are proved on the inverse equivalences, base_map_symm and total_map_symm, where the two sides agree by unfolding.

Main definitions

• FamHom — the morphisms of Fam(Type) proper, with FamHom.id, FamHom.comp and the map of total spaces FamHom.total.

• fibreValueMap — the functoriality of the slice functor's fibre in the family.

• codeMap — the action of the code's interpretation on a morphism of families.

• arrowHom — the morphism of walking-arrow presheaves of a commuting square over a base change.

• famHomOfNatTrans, natTransOfFamHom — the two directions between morphisms of walking-arrow presheaves and of families.

Main statements

• codeMap_id, codeMap_comp — the action is functorial.

• base_map, total_map — the isomorphism of GebProto.­LargeIR.­arrowPshCodeEquiv is natural in the input presheaf, at each of the two levels.

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.

Tags

prototype, presheaf, walking arrow, inductive-recursive, code, positive, naturality

Morphisms of families

The action of the code on morphisms

Morphisms of walking-arrow presheaves and of families

Naturality of the isomorphism