The category of IR codes

Corollary 2 of [HancockMcBrideGhaniMalatestaAltenkirch2013]: IR codes and the homsets of Definition 8 form a category. Composition is transferred through the full-and-faithful interpretation of Theorem 3 — the code morphism carried by the vertical composite of the interpreted transformations — and the category laws follow from the vertical laws together with the round-trip laws of the Theorem 3 equivalence. The identity laws additionally consume the identity-image equation IR.interpHom_id, proved by induction on the domain code over the stack of IR.preUnitStack, against the semantic counterpart of that stack: an iterated coproduct tower with its iterated Lemma 4 isomorphism.

Main definitions

IR.mplus, IR.mplusInj, IR.mplusMorMap — the iterated coproduct object of a stack of superscripts, its iterated injection, and its action on morphisms.

IR.mprecompIso — the iterated Lemma 4 isomorphism between the interpretation of an iterated precomposition and the interpretation at IR.mplus.

IR.preUnitComponent — the semantic pre-unit component: the interpretation image of IR.mplusInj, composed with the inverse of IR.mprecompIso.

IR.interpHomDeltaSummand — the per-summand transport of the δ-domain case of IR.interpHomEquiv.

IR.interpHomIotaComposite, IR.interpHomIotaCast — the ι-branch equivalence of the Theorem 3 step and its transport along a code equality.

IR.deltaEmptyWeight, IR.deltaEmptyInj — the canonical weight out of the lift of an empty-witnessed family, and the semantic inclusion of the empty-witnessed summand into the δ interpretation.

IR.deltaEmptySummandHom — the transported summand isomorphism of the Lemma 4 δ-square at that inclusion.

IR.navWeight, IR.navReindex — the tower navigation weight, and the reindexing of a lifted direction family along the inclusion of the all-unresolved classifier's subtype.

IR.navInj — the tower-conjugated navigation inclusion.

IR.navBridgeMor — the tower morphism induced by a weight at a right-appended superscript.

IR.comp — composition of code morphisms: the code morphism carried by the vertical composite of the interpreted transformations.

Main statements

IR.mprecompIso_natural — naturality of the tower isomorphism in the interpreted object.

IR.interpHom_sigmaPush — IR.interpHom sends IR.sigmaPush to composition with the semantic σ-injection.

IR.interpHom_deltaEmptyPush — IR.interpHom sends IR.deltaEmptyPush to composition with the semantic empty-summand inclusion.

IR.interpHom_msigmaPush, IR.interpHom_deltaNav — IR.interpHom sends the stack σ-push and the tower navigation to composition with the corresponding semantic inclusion.

IR.interpHom_preUnitStack — IR.interpHom sends IR.preUnitStack to the semantic pre-unit component, by IR.induction on the domain code.

IR.interpHom_comp, IR.interpHom_id — IR.interpHom sends IR.comp to the vertical composite and IR.id to the identity transformation: the interpretation is functorial on morphisms.

IR.id_comp, IR.comp_id, IR.comp_assoc — the category laws of Corollary 2 of [HancockMcBrideGhaniMalatestaAltenkirch2013].

Implementation notes

The tower constructions recurse on the stack through List.rec, not on codes; the snoc lemmas are the corresponding List.rec inductions, with the motive quantified over the code where the recursion changes it (IR.mprecompIso and its snoc lemmas). Object equalities entering the tower (IR.mplus_snoc, IR.mprecomp_snoc) are carried as FreeCoprodCompDisc.isoOfEq transports and commuted across the Lemma 4 isomorphism by elimination of the generalized equality.

References

[HancockMcBrideGhaniMalatestaAltenkirch2013]

Tags

inductive-recursive, morphism, category

The semantic tower

The iterated coproduct object: fold plus over the stack.

mplus at a right-appended superscript feeds the coproduct at the inner position.

The iterated right injection into mplus.

The iterated Lemma 4 isomorphism between the interpretation of an iterated precomposition and the interpretation at mplus.

The semantic pre-unit component: the interpretation image of the iterated injection, composed with the inverse of the iterated Lemma 4 isomorphism.

At the empty stack the semantic pre-unit component is the identity.

Transport of a composite with a fresh right injection along an equality of the inner object, by elimination of the generalized equality: the cast passes to the left factor.

IR.mplusInj at a right-appended superscript, transported along IR.mplus_snoc: the fresh inner injection followed by the tower injection at the enlarged base.

The Lemma 4 isomorphism commutes object-equality transports across its two sides (forward direction), by elimination of the generalized equality.

The Lemma 4 isomorphism commutes object-equality transports across its two sides (inverse direction), by elimination of the generalized equality.

The forward component of IR.mprecompIso at a right-appended superscript: one Lemma 4 layer at the base of the tower, conjugated by the IR.mprecomp_snoc and IR.mplus_snoc transports.

The inverse component of IR.mprecompIso at a right-appended superscript: the inverse of one Lemma 4 layer at the base of the tower, conjugated by the IR.mplus_snoc and IR.mprecomp_snoc transports.