T = U <~> (components_of T == components_of U). Proof. econstructor. econstructor. exact eisadj_path_natural_transformation. Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Equivalences HoTT.Types Trunc Basics.Tactics.