fact: Definition Build_Transform' (transform' : forall x, F x ~> G x) (natural : forall x y (f : x ~> y), fmap[G] f ∘ transform' x ≈ transform' y ∘ fmap[F] f) : Transform.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor