`{Funext} (C D : PreCategory) : forall x : path_precategory''_T C D, path_precategory_uncurried'_inv (path_precategory_uncurried' C D x) = x. Proof. destruct C, D; cbn in *. intros [H0' [H1' [H2' H3']]]. path_induction. cbn. repeat (edestruct (center (_ = _)); try reflexivity). Qed.
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.