equiv_path_precategory_uncurried' `{Funext} (C D : PreCategory) : path_precategory''_T C D <~> C = D. Proof. apply (equiv_adjointify (@path_precategory_uncurried' _ C D) (@path_precategory_uncurried'_inv C D)). - hnf. intros []. apply path_precategory_uncurried'_idpath. - hnf. apply __eissect. 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.