2-cell specifications

A natural transformation between two functor specifications with the same source and target is specified by a component at each object index and a Bool equation asserting naturality. The component ranges over the target's full hom type from the outset, so the identity 2-cell has every component an identity.

The 2-cells between a fixed pair of functor specifications form a category under componentwise composition, and each of them generates a mathlib natural transformation between the generated functors.

Main definitions

CategoryTheory.FinCat.Hom₂.natCheckOf, CategoryTheory.FinCat.Hom₂.natCheck — the decidable naturality check on client morphisms.

CategoryTheory.FinCat.Hom₂ — the 2-cell specification type.

CategoryTheory.FinCat.Hom.instCategory — the hom-category: vertical composition and the identity 2-cell.

CategoryTheory.FinCat.Hom₂.toNatTrans — the mathlib natural transformation a 2-cell specification generates.

Main statements

FinCat.Hom₂.natCheck_eq_true_iff — the check reflects naturality on client morphisms.

FinCat.Hom₂.eq_of_app_eq, FinCat.Hom₂.ext — extensionality, at FinCat.Hom₂ F G and at F ⟶ G respectively.

FinCat.Hom₂.app_id, FinCat.Hom₂.app_comp — the components of the identity 2-cell and of a vertical composite.

FinCat.Hom₂.natCheck_total — naturality, on all morphisms.

Implementation notes

natCheckOf precedes the structure because the natValid field's type mentions it. The enclosing namespace FinCat stays open throughout; the inner namespace Hom₂ blocks close around structure Hom₂, which cannot be declared inside a namespace of its own name, and around instance Hom.instCategory, whose full name is a FinCat.Hom name and so cannot be written inside a namespace Hom₂ either.

eq_of_app_eq precedes the category instance because the instance's three law fields need it and the hom notation ⟶ does not exist until the instance does. CategoryTheory.Cat.Hom.instCategory discharges its counterparts by congrArg, which is available there because CategoryTheory.Cat.Hom₂ is a one-field wrapper; FinCat.Hom is not such a bundling, so that route is unavailable here.

natCheck_total extends the check off the client range, as FinCat.Hom.mapTotal_compTotal does for the composition check. The extension, rather than the check itself, is what toNatTrans needs: a morphism of the generated category is an arbitrary element of the full hom type, not an embedded client morphism.

toNatTrans states its result type as CategoryTheory.NatTrans rather than through ⟶. The two are the same type, but the notation names it via CategoryTheory.Functor.category, whose category laws are discharged by aesop_cat and so depend on Classical.choice; the notation therefore carries that dependence into the type of any declaration written with it.

The check is stated over the total composition and the total morphism maps, for the reason FinCat.Hom.compCheckOf is: a client composite may land on the reserved identity index, on which the client's morphism map is undefined.

FinCat.Hom₂ is not marked @[ext]. A structure-derived extensionality lemma does not fire on goals stated through the hom notation F ⟶ G, so it would be unusable at the only place it is needed; the name FinCat.Hom₂.ext is left free for a hand-written lemma phrased at F ⟶ G, matching what mathlib does for CategoryTheory.Cat.Hom₂.

References

[JohnsonYau2021] § 1.1 — the notion of natural transformation, of which this module's specification type is a presentation.

Tags

category, functor, natural transformation, finite category, decidable, constructive, choice-free

Naturality, as a Bool, on client morphisms. Stated over the total composition and the total morphism maps, for the reason FinCat.Hom.compCheckOf is.

A 2-cell specification: a natural transformation between two functor specifications.

The component at each object. It ranges over the full hom type from the outset, the identity 2-cell having every component an identity.

Naturality.

The naturality check reflects naturality on client morphisms.

α's naturality check.

Two 2-cells with equal components are equal. Stated at FinCat.Hom₂ F G rather than at F ⟶ G, so that it is available before the hom-category instance exists.

The category of 2-cells between two functor specifications: vertical composition and the identity 2-cell.

The identity 2-cell's components are the reserved identities.

A vertical composite's components are the composites.

Two 2-cells with equal components are equal, phrased at F ⟶ G so that the ext tactic fires on goals stated through the hom notation.

Naturality at total morphisms, extending natCheck off the client range.