- app : Π (X : C), F.obj X ⟶ G.obj X
- naturality' : (∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ c.app Y = c.app X ≫ G.map f) . "obviously"
nat_trans F G represents a natural transformation between functors
app provides the components of the natural transformation.
Naturality is expressed by
nat_trans.id F is the identity natural transformation on a functor
vcomp α β is the vertical compositions of natural transformations.