pr1_mor o sig_functor_mor = pr1' := idpath. End sig_mor. Arguments pr1_mor {A Pmor _ Pidentity Pcompose P_associativity P_left_identity P_right_identity}. Section sig_mor_hProp. Variable A : PreCategory. Variable Pmor : forall s d, morphism A s d -> Type. Local Notation mor s d := (sig_type (Pmor s d)). Context `(HPmor : forall s d m, IsHProp (Pmor s d m)). Variable Pidentity : forall x, @Pmor x x (@identity A _). Variable Pcompose : forall s d d' m1 m2, @Pmor d d' m1 -> @Pmor s d m2 -> @Pmor s d' (m1 o m2). Local Notation identity x := (@identity A x; @Pidentity x). Local Notation compose m1 m2 := (m1.1 o m2.1; @Pcompose _ _ _ m1.1 m2.1 m1.2 m2.2)%morphism. Local Ltac t ex_tac := intros; simpl; apply path_sigma_uncurried; simpl; ex_tac; apply path_ishprop. Let P_associativity : forall x1 x2 x3 x4 (m1 : mor x1 x2) (m2 : mor x2 x3) (m3 : mor x3 x4), compose (compose m3 m2) m1 = compose m3 (compose m2 m1). Proof. abstract t ltac:(exists (associativity _ _ _ _ _ _ _ _)) using P_associativity_on_morphisms_subproof. Defined.
Require Import HoTT.Tactics Types.Forall Types.Sigma Basics.Trunc. Require Import Category.Core Functor.Core Category.Sigma.Core. Require Import Functor.Paths. Import Functor.Identity.FunctorIdentityNotations. Import Functor.Composition.Core.FunctorCompositionCoreNotations.