nat_trans 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_lemma.

nat_trans.id F is the identity natural transformation on a functor F.

vcomp α β is the vertical compositions of natural transformations.