proposition: Lemma path'_natural_transformation : components_of T = components_of U -> T = U.
proof: Proof. intros. destruct T, U; simpl in *. path_induction. f_ap; refine (center _). Qed.
imports: Category.Core Functor.Core NaturalTransformation.Core Equivalences HoTT.Types Trunc Basics.Tactics