proposition: Lemma equiv_path_precategory_uncurried'__eissect `{Funext} (C D : PreCategory) : forall x : path_precategory''_T C D, path_precategory_uncurried'_inv (path_precategory_uncurried' C D x) = x.
proof: Proof. destruct C, D; cbn in *. intros [H0' [H1' [H2' H3']]]. path_induction. cbn. repeat (edestruct (center (_ = _)); try reflexivity). Qed.
imports: Category.Core HoTT.Basics.Equivalences HoTT.Basics.PathGroupoids HoTT.Basics.Trunc HoTT.Basics.Tactics HoTT.Types.Sigma HoTT.Types.Arrow HoTT.Types.Forall HoTT.Tactics