(** * ∑-categories on morphisms - a category with the same objects, but a ∑ type for morphisms *)
Require Import HoTT.Tactics Types.Forall Types.Sigma Basics.Trunc.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Category.Core Functor.Core Category.Sigma.Core.
Require Functor.Composition.Core Functor.Identity.
Require Import Functor.Paths.
Import Functor.Identity.FunctorIdentityNotations.
Import Functor.Composition.Core.FunctorCompositionCoreNotations.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

Local Notation sig_type := Overture.sig.
Local Notation pr1_type := Overture.pr1.

Local Open Scope morphism_scope.
Local Open Scope functor_scope.

Section sig_mor.
  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, IsHSet (mor s d)).

  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.

  Hypothesis 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).

  Hypothesis P_left_identity
  : forall a b (f : mor a b),
      compose (identity b) f = f.

  Hypothesis P_right_identity
  : forall a b (f : mor a b),
      compose f (identity a) = f.

  (** ** Definition of [sig_mor]-precategory *)
  Definition sig_mor' : PreCategory.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
PreCategory
  Proof.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
PreCategory
    refine (@Build_PreCategory
              (object A)
              (fun s d => mor s d)
              (fun x => identity x)
              (fun s d d' m1 m2 => compose m1 m2)
              _
              _
              _
              _);
    assumption.
  Defined.

  (** ** First projection functor *)
  Definition pr1_mor : Functor sig_mor' A
    := Build_Functor
         sig_mor' A
         idmap
         (fun _ _ => @pr1_type _ _)
         (fun _ _ _ _ _ => idpath)
         (fun _ => idpath).

  Definition sig_mor_as_sig : PreCategory.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
PreCategory
  Proof.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
PreCategory
    refine (@sig' A (fun _ => Unit) (fun s d => @Pmor (pr1_type s) (pr1_type d)) _ (fun _ => Pidentity _) (fun _ _ _ _ _ m1 m2 => Pcompose m1 m2) _ _ _);
    intros; trivial.
  Defined.

  Definition sig_functor_mor : Functor sig_mor_as_sig sig_mor'
    := Build_Functor
         sig_mor_as_sig sig_mor'
         (@pr1_type _ _)
         (fun _ _ => idmap)
         (fun _ _ _ _ _ => idpath)
         (fun _ => idpath).

  Definition sig_functor_mor_inv : Functor sig_mor' sig_mor_as_sig
    := Build_Functor
         sig_mor' sig_mor_as_sig
         (fun x => exist _ x tt)
         (fun _ _ => idmap)
         (fun _ _ _ _ _ => idpath)
         (fun _ => idpath).

  Local Open Scope functor_scope.

  Lemma sig_mor_eq `{Funext}
  : sig_functor_mor o sig_functor_mor_inv = 1
    /\ sig_functor_mor_inv o sig_functor_mor = 1.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: Funext
(sig_functor_mor o sig_functor_mor_inv = 1) *
(sig_functor_mor_inv o sig_functor_mor = 1)
  Proof.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: Funext
(sig_functor_mor o sig_functor_mor_inv = 1) *
(sig_functor_mor_inv o sig_functor_mor = 1)
    split; path_functor; simpl; trivial.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: Funext
sig_type
  (fun
     HO : (fun c : sig_type (fun _ : A => Unit) =>
           (pr1_type c; tt)) = idmap =>
   transport
     (fun
        GO : sig_type (fun _ : A => Unit) ->
             sig_type (fun _ : A => Unit) =>
      forall s d : sig_type (fun _ : A => Unit),
      mor (pr1_type s) (pr1_type d) ->
      mor (pr1_type (GO s)) (pr1_type (GO d))) HO
     (fun s d : sig_type (fun _ : A => Unit) => idmap) =
   (fun s d : sig_type (fun _ : A => Unit) => idmap))
    refine (exist
              _
              (path_forall
                 _
                 _
                 (fun x
                  => match x as x return (x.1; tt) = x with
                       | (_; tt) => idpath
                     end))
              _).
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: Funext
transport
  (fun
     GO : sig_type (fun _ : A => Unit) ->
          sig_type (fun _ : A => Unit) =>
   forall s d : sig_type (fun _ : A => Unit),
   mor (pr1_type s) (pr1_type d) ->
   mor (pr1_type (GO s)) (pr1_type (GO d)))
  (path_forall
     (fun x : sig_type (fun _ : A => Unit) =>
      (pr1_type x; tt)) idmap
     (fun x : sig_type (fun _ : A => Unit) =>
      let x0 := x in
      let proj1 := pr1_type x0 in
      let proj2 := x0.2 in
      match
        proj2 as proj3
        return
          ((pr1_type (proj1; proj3); tt) =
           (proj1; proj3))
      with
      | tt => 1%path
      end))
  (fun s d : sig_type (fun _ : A => Unit) => idmap) =
(fun s d : sig_type (fun _ : A => Unit) => idmap)
    repeat (apply path_forall; intro).
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity: forall (a b : A) (f : mor a b),
compose (identity b) f = f
P_right_identity: forall (a b : A) (f : mor a b),
compose f (identity a) = f
H: Funext
x, x0: sig_type (fun _ : A => Unit)
x1: mor (pr1_type x) (pr1_type x0)
transport
  (fun
     GO : sig_type (fun _ : A => Unit) ->
          sig_type (fun _ : A => Unit) =>
   forall s d : sig_type (fun _ : A => Unit),
   mor (pr1_type s) (pr1_type d) ->
   mor (pr1_type (GO s)) (pr1_type (GO d)))
  (path_forall
     (fun x : sig_type (fun _ : A => Unit) =>
      (pr1_type x; tt)) idmap
     (fun x : sig_type (fun _ : A => Unit) =>
      let x0 := x in
      let proj1 := pr1_type x0 in
      let proj2 := x0.2 in
      match
        proj2 as proj3
        return
          ((pr1_type (proj1; proj3); tt) =
           (proj1; proj3))
      with
      | tt => 1%path
      end))
  (fun s d : sig_type (fun _ : A => Unit) => idmap) x
  x0 x1 = x1
    destruct_head @sig_type.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
((pr1_type m3 o pr1_type m2
  o pr1_type m1)%morphism;
Pcompose (Pcompose m3.2 m2.2) m1.2) =
((pr1_type m3
  o (pr1_type m2 o pr1_type m1))%morphism;
Pcompose m3.2 (Pcompose m2.2 m1.2))
P_left_identity: forall (a b : A) (f : mor a b),
((1 o pr1_type f)%morphism;
Pcompose (Pidentity b) f.2) = f
P_right_identity: forall (a b : A) (f : mor a b),
((pr1_type f o 1)%morphism;
Pcompose f.2 (Pidentity a)) = f
H: Funext
proj4: A
proj5: Unit
proj0: A
proj3: Unit
proj1: morphism A proj4 proj0
proj2: Pmor proj4 proj0 proj1
transport
  (fun
     GO : sig_type (fun _ : A => Unit) ->
          sig_type (fun _ : A => Unit) =>
   forall s d : sig_type (fun _ : A => Unit),
   mor (pr1_type s) (pr1_type d) ->
   mor (pr1_type (GO s)) (pr1_type (GO d)))
  (path_forall
     (fun x : sig_type (fun _ : A => Unit) =>
      (pr1_type x; tt)) idmap
     (fun x : sig_type (fun _ : A => Unit) =>
      match
        x.2 as proj2
        return
          ((pr1_type x; tt) = (pr1_type x; proj2))
      with
      | tt => 1%path
      end))
  (fun s d : sig_type (fun _ : A => Unit) => idmap)
  (proj4; proj5) (proj0; proj3) (proj1; proj2) =
(proj1; proj2)
    destruct_head Unit.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
((pr1_type m3 o pr1_type m2
  o pr1_type m1)%morphism;
Pcompose (Pcompose m3.2 m2.2) m1.2) =
((pr1_type m3
  o (pr1_type m2 o pr1_type m1))%morphism;
Pcompose m3.2 (Pcompose m2.2 m1.2))
P_left_identity: forall (a b : A) (f : mor a b),
((1 o pr1_type f)%morphism;
Pcompose (Pidentity b) f.2) = f
P_right_identity: forall (a b : A) (f : mor a b),
((pr1_type f o 1)%morphism;
Pcompose f.2 (Pidentity a)) = f
H: Funext
proj4, proj0: A
proj1: morphism A proj4 proj0
proj2: Pmor proj4 proj0 proj1
transport
  (fun
     GO : sig_type (fun _ : A => Unit) ->
          sig_type (fun _ : A => Unit) =>
   forall s d : sig_type (fun _ : A => Unit),
   mor (pr1_type s) (pr1_type d) ->
   mor (pr1_type (GO s)) (pr1_type (GO d)))
  (path_forall
     (fun x : sig_type (fun _ : A => Unit) =>
      (pr1_type x; tt)) idmap
     (fun x : sig_type (fun _ : A => Unit) =>
      match
        x.2 as proj2
        return
          ((pr1_type x; tt) = (pr1_type x; proj2))
      with
      | tt => 1%path
      end))
  (fun s d : sig_type (fun _ : A => Unit) => idmap)
  (proj4; tt) (proj0; tt) (proj1; proj2) =
(proj1; proj2)
    rewrite !transport_forall_constant.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
((pr1_type m3 o pr1_type m2
  o pr1_type m1)%morphism;
Pcompose (Pcompose m3.2 m2.2) m1.2) =
((pr1_type m3
  o (pr1_type m2 o pr1_type m1))%morphism;
Pcompose m3.2 (Pcompose m2.2 m1.2))
P_left_identity: forall (a b : A) (f : mor a b),
((1 o pr1_type f)%morphism;
Pcompose (Pidentity b) f.2) = f
P_right_identity: forall (a b : A) (f : mor a b),
((pr1_type f o 1)%morphism;
Pcompose f.2 (Pidentity a)) = f
H: Funext
proj4, proj0: A
proj1: morphism A proj4 proj0
proj2: Pmor proj4 proj0 proj1
transport
  (fun
     x : sig_type (fun _ : A => Unit) ->
         sig_type (fun _ : A => Unit) =>
   mor (pr1_type (x (proj4; tt)))
     (pr1_type (x (proj0; tt))))
  (path_forall
     (fun x : sig_type (fun _ : A => Unit) =>
      (pr1_type x; tt)) idmap
     (fun x : sig_type (fun _ : A => Unit) =>
      match
        x.2 as proj2
        return
          ((pr1_type x; tt) = (pr1_type x; proj2))
      with
      | tt => 1%path
      end)) (proj1; proj2) = (proj1; proj2)
    transport_path_forall_hammer.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall s d : A, IsHSet (mor s d)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
((pr1_type m3 o pr1_type m2
  o pr1_type m1)%morphism;
Pcompose (Pcompose m3.2 m2.2) m1.2) =
((pr1_type m3
  o (pr1_type m2 o pr1_type m1))%morphism;
Pcompose m3.2 (Pcompose m2.2 m1.2))
P_left_identity: forall (a b : A) (f : mor a b),
((1 o pr1_type f)%morphism;
Pcompose (Pidentity b) f.2) = f
P_right_identity: forall (a b : A) (f : mor a b),
((pr1_type f o 1)%morphism;
Pcompose f.2 (Pidentity a)) = f
H: Funext
proj4, proj0: A
proj1: morphism A proj4 proj0
proj2: Pmor proj4 proj0 proj1
transport
  (fun y : sig_type (fun _ : A => Unit) =>
   mor (pr1_type (proj4; tt)) (pr1_type y)) 1
  (transport
     (fun y : sig_type (fun _ : A => Unit) =>
      mor (pr1_type y)
        (pr1_type (pr1_type (proj0; tt); tt))) 1
     (proj1; proj2)) = (proj1; proj2)
    reflexivity.
  Qed.

  Definition sig_mor_compat : 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).
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall (s d : A) (m : morphism A s d),
IsHProp (Pmor s d m)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
forall (x1 x2 x3 x4 : A) (m1 : mor x1 x2)
(m2 : mor x2 x3) (m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
  Proof.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall (s d : A) (m : morphism A s d),
IsHProp (Pmor s d m)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
forall (x1 x2 x3 x4 : A) (m1 : mor x1 x2)
(m2 : mor x2 x3) (m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
    abstract t ltac:(exists (associativity _ _ _ _ _ _ _ _))
      using P_associativity_on_morphisms_subproof.
  Defined.

  Let P_left_identity
  : forall a b (f : mor a b),
      compose (identity b) f = f.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall (s d : A) (m : morphism A s d),
IsHProp (Pmor s d m)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity:= P_associativity_on_morphisms_subproof: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
forall (a b : A) (f : mor a b),
compose (identity b) f = f
  Proof.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall (s d : A) (m : morphism A s d),
IsHProp (Pmor s d m)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity:= P_associativity_on_morphisms_subproof: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
forall (a b : A) (f : mor a b),
compose (identity b) f = f
    clear P_associativity.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall (s d : A) (m : morphism A s d),
IsHProp (Pmor s d m)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
forall (a b : A) (f : mor a b),
compose (identity b) f = f
    abstract t ltac:(exists (left_identity _ _ _ _))
      using P_left_identity_on_morphisms_subproof.
  Defined.

  Let P_right_identity
  : forall a b (f : mor a b),
      compose f (identity a) = f.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall (s d : A) (m : morphism A s d),
IsHProp (Pmor s d m)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity:= P_associativity_on_morphisms_subproof: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity:= P_left_identity_on_morphisms_subproof: forall (a b : A) (f : mor a b),
compose (identity b) f = f
forall (a b : A) (f : mor a b),
compose f (identity a) = f
  Proof.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall (s d : A) (m : morphism A s d),
IsHProp (Pmor s d m)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
P_associativity:= P_associativity_on_morphisms_subproof: forall (x1 x2 x3 x4 : A)
(m1 : mor x1 x2) (m2 : mor x2 x3)
(m3 : mor x3 x4),
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
P_left_identity:= P_left_identity_on_morphisms_subproof: forall (a b : A) (f : mor a b),
compose (identity b) f = f
forall (a b : A) (f : mor a b),
compose f (identity a) = f
    clear P_associativity P_left_identity.
A: PreCategory
Pmor: forall s d : A, morphism A s d -> Type
HPmor: forall (s d : A) (m : morphism A s d),
IsHProp (Pmor s d m)
Pidentity: forall x : A, Pmor x x 1
Pcompose: forall (s d d' : A) (m1 : morphism A d d')
(m2 : morphism A s d),
Pmor d d' m1 ->
Pmor s d m2 -> Pmor s d' (m1 o m2)
forall (a b : A) (f : mor a b),
compose f (identity a) = f
    abstract t ltac:(exists (right_identity _ _ _ _))
      using P_right_identity_on_morphisms_subproof.
  Defined.

  (** ** Definition of [sig_mor]-precategory *)
  Definition sig_mor : PreCategory
    := Eval cbv delta [P_associativity P_left_identity P_right_identity]
      in @sig_mor' A Pmor _ Pidentity Pcompose P_associativity P_left_identity P_right_identity.

  (** ** First projection functor *)
  Definition proj1_sig_mor : Functor sig_mor A
    := pr1_mor.
End sig_mor_hProp.

Arguments proj1_sig_mor {A Pmor HPmor Pidentity Pcompose}.