components_of T = components_of U -> T = U. Proof. intros. destruct T, U; simpl in *. path_induction. f_ap; refine (center _). Qed.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Equivalences HoTT.Types Trunc Basics.Tactics.