proposition: Lemma equiv_path_natural_transformation : T = U <~> (components_of T == components_of U).
proof: Proof. econstructor. econstructor. exact eisadj_path_natural_transformation. Defined.
imports: Category.Core Functor.Core NaturalTransformation.Core Equivalences HoTT.Types Trunc Basics.Tactics