(C D : PreCategory) : C = D -> path_precategory''_T C D. Proof. intro H'. exists (ap object H'). exists ((transport_compose _ object _ _) ^ @ apD (@morphism) H'). split. - refine (_ @ apD (@compose) H'); cbn. refine (transport_pp _ _ _ _ @ _). refine ((ap _ (transportD_compose (fun obj => obj -> obj -> Type) (fun obj mor => forall s d d' : obj, mor d d' -> mor s d -> mor s d') object H' (morphism C) (@compose C))^) @ (transport_apD_transportD _ morphism (fun x mor => forall s d d' : x, mor d d' -> mor s d -> mor s d') H' (@compose C))). - refine (_ @ apD (@identity) H'); cbn. refine (transport_pp _ _ _ _ @ _). refine ((ap _ (transportD_compose (fun obj => obj -> obj -> Type) (fun obj mor => forall x : obj, mor x x) object H' (morphism C) (@identity C))^) @ (transport_apD_transportD _ morphism (fun x mor => forall s : x, mor s s) H' (@identity C))). 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.