Natural transformations #
Defines natural transformations between functors.
A natural transformation α : NatTrans F G
consists of morphisms α.app X : F.obj X ⟶ G.obj X⟶ G.obj X
,
and the naturality squares α.naturality f : F.map f ≫ α.app Y = α.app X ≫ G.map f≫ α.app Y = α.app X ≫ G.map f≫ G.map f
,
where f : X ⟶ Y⟶ Y
.
Note that we make NatTrans.naturality
a simp lemma, with the preferred simp normal form
pushing components of natural transformations to the left.
See also CategoryTheory.FunctorCat
, where we provide the category structure on
functors and natural transformations.
Introduces notations
τ.app X
for the components of natural transformations,F ⟶ G⟶ G
for the type of natural transformations between functorsF
andG
(this and the next requireCategoryTheory.FunctorCat
),σ ≫ τ≫ τ
for vertical compositions, andσ ◫ τ◫ τ
for horizontal compositions.
The component of a natural transformation.
app : (X : C) → F.obj X ⟶ G.obj XThe naturality square for a given morphism.
NatTrans F G
represents a natural transformation between functors F
and G
.
The field app
provides the components of the natural transformation.
Naturality is expressed by α.naturality
.
Instances For
This unexpander will pretty print η.app X
properly.
Without this, we would have NatTrans.app η X
.
Equations
- One or more equations did not get rendered due to their size.
NatTrans.id F
is the identity natural transformation on a functor F
.
Equations
- CategoryTheory.NatTrans.id F = CategoryTheory.NatTrans.mk fun X => 𝟙 (F.obj X)
Equations
- CategoryTheory.NatTrans.instInhabitedNatTrans F = { default := CategoryTheory.NatTrans.id F }
vcomp α β
is the vertical compositions of natural transformations.
Equations
- CategoryTheory.NatTrans.vcomp α β = CategoryTheory.NatTrans.mk fun X => α.app X ≫ β.app X