pr1' : Functor sig' A := Build_Functor sig' A (@pr1 _ _) (fun _ _ => @pr1 _ _) (fun _ _ _ _ _ => idpath) (fun _ => idpath). End sig_obj_mor. Arguments pr1' {A Pobj Pmor HPmor Pidentity Pcompose P_associativity P_left_identity P_right_identity}. Section sig_obj_mor_hProp. Variable A : PreCategory. Variable Pobj : A -> Type. Local Notation obj := (sig_type Pobj). Variable Pmor : forall s d : obj, morphism A s.1 d.1 -> 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.1; @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_core_subproof. Defined.
Require Import Category.Core Functor.Core. Require Import Basics.Trunc Types.Sigma.