path_precategory_uncurried' `{fs : Funext} (C D : PreCategory) : path_precategory''_T C D -> C = D. Proof. intros [? [? [? ?]]]. destruct C, D; cbn in *. path_induction; cbn in *. f_ap; eapply @center; abstract exact _. Defined.
Require Import Category.Core. Require Import HoTT.Basics.Equivalences HoTT.Basics.PathGroupoids HoTT.Basics.Trunc HoTT.Basics.Tactics. Require Import HoTT.Types.Sigma HoTT.Types.Arrow HoTT.Types.Forall. Require Import HoTT.Tactics.