components_of T == components_of U -> T = U. Proof. intros. apply path'_natural_transformation. apply path_forall; assumption. Qed.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Equivalences HoTT.Types Trunc Basics.Tactics.