NaturalTransformation (F * G) (F' * G') := Build_NaturalTransformation (F * G) (F' * G') (fun x : A => (T x, U x)) (fun _ _ _ => path_prod' (commutes T _ _ _) (commutes U _ _ _)).
Require Import Category.Core Functor.Core Category.Prod Functor.Prod.Core NaturalTransformation.Core. Require Import Types.Prod.