path_precategory' `{fs : Funext} (C D : PreCategory) : forall (Hobj : object C = object D) (Hmor : transport (fun obj => obj -> obj -> Type) Hobj (morphism C) = morphism D), transport _ Hmor (transportD (fun obj => obj -> obj -> Type) (fun obj mor => forall s d d', mor d d' -> mor s d -> mor s d') Hobj (morphism C) (@compose C)) = @compose D -> C = D. Proof. intros. apply path_precategory_uncurried. repeat esplit; eassumption. 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.