proposition: Lemma path_natural_transformation : components_of T == components_of U -> T = U.
proof: Proof. intros. apply path'_natural_transformation. apply path_forall; assumption. Qed.
imports: Category.Core Functor.Core NaturalTransformation.Core Equivalences HoTT.Types Trunc Basics.Tactics