CoreLaws.v

Require Import Functor.Core NaturalTransformation.Core.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Category.Strict.
Require Import Functor.Composition.Core.
Require Import NaturalTransformation.Paths NaturalTransformation.Composition.Core.
Require Import Category.Morphisms FunctorCategory.Core.
Require Import Pseudofunctor.Core Pseudofunctor.RewriteLaws.
Require Import NaturalTransformation.Composition.Laws.
Require Import FunctorCategory.Morphisms.
Require LaxComma.CoreParts.
Require Import HoTT.Tactics.

Import Functor.Identity.FunctorIdentityNotations.

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


Local Open Scope morphism_scope.
Local Open Scope category_scope.

(** Quoting David Spivak:

    David: ok
       so an object of [FC ⇓ D] is a pair [(X, G)], where [X] is a
       finite category (or a small category or whatever you wanted)
       and [G : X --> D] is a functor.
       a morphism in [FC ⇓ D] is a ``natural transformation diagram''
       (as opposed to a commutative diagram, in which the natural
       transformation would be ``identity'')
       so a map in [FC ⇓ D] from [(X, G)] to [(X', G')] is a pair
       [(F, α)] where [F : X --> X'] is a functor and
       [α : G --> G' ∘ F] is a natural transformation
       and the punchline is that there is a functor
       [colim : FC ⇓ D --> D]

     David: consider for yourself the case where [F : X --> X'] is
       identity ([X = X']) and (separately) the case where
       [α : G --> G ∘ F] is identity.
       the point is, you've already done the work to get this colim
       functor.
       because every map in [FC ⇓ D] can be written as a composition
       of two maps, one where the [F]-part is identity and one where
       the [α]-part is identity.
       and you've worked both of those cases out already.
       *)

Module Import LaxCommaCategory.
  Include LaxComma.CoreParts.LaxCommaCategoryParts.
  Section lax_comma_category_parts.
    Context `{Funext}.
    Variables A B : PreCategory.

    Variable S : Pseudofunctor A.
    Variable T : Pseudofunctor B.

    Context `{forall a b, IsHSet (Functor (S a) (T b))}.

    Local Notation object := (@object _ A B S T).
    Local Notation morphism := (@morphism _ A B S T).
    Local Notation compose := (@compose _ A B S T).
    Local Notation identity := (@identity _ A B S T).

    Local Ltac t_do_work :=
      repeat match goal with
               | _ => reflexivity
               | [ |- context[components_of ?T^-1 ?x] ]
                 => progress change (T^-1 x) with ((T x)^-1)
               | [ |- context[?F _1 ?m^-1] ]
                 => progress change (F _1 m^-1) with ((F _1 m)^-1)
               | _ => progress repeat iso_collapse_inverse_right'
             end.

    Local Ltac t_start :=
      simpl in *;
      repeat match goal with
               | [ H : ?x = _ |- _ ] => rewrite H; clear H; try clear x
             end;
      path_natural_transformation;
      simpl in *;
      rewrite !Category.Core.left_identity, !Category.Core.right_identity;
      rewrite !composition_of.

    Local Ltac t :=
      t_start;
      rewrite <- !Category.Core.associativity;
      (** A reflective simplifier would be really useful here... *)
      repeat match goal with
               | _ => progress t_do_work
               | [ |- context[components_of ?T ?x] ]
                 => simpl rewrite <- !(commutes_pT_F T)
               | [ |- context[components_of ?T ?x] ]
                 => simpl rewrite <- !(commutes T)
               | _ => iso_move_inverse
             end.

    (** Ugh. The following code constructs the type of the helper lemma:
<<
      Lemma associativity x1 x2 x3 x4
            (m1 : morphism x1 x2) (m2 : morphism x2 x3) (m3 : morphism x3 x4)
      : compose (compose m3 m2) m1 = compose m3 (compose m2 m1).
      Proof.
        exact (@path_morphism' _ _
                                (compose (compose m3 m2) m1)
                                (compose m3 (compose m2 m1))
                                (Category.Core.associativity _ _ _ _ _ _ _ _)
                                (Category.Core.associativity _ _ _ _ _ _ _ _)
                                _).
        simpl in *.
        repeat match goal with
                 | [ |- context[@morphism_inverse
                                     _ _ _ _
                                     (@isisomorphism_isomorphic
                                        _ _ _
                                        (Category.Morphisms.idtoiso
                                           ?C0
                                           (ap (p_morphism_of ?F (s:=_) (d:=_))
                                               (Category.Core.associativity ?C ?x1 ?x2 ?x3 ?x4 ?m1 ?m2 ?m3))))] ]
                   => generalize (@p_composition_of_coherent_inverse_for_rewrite _ C F x1 x2 x3 x4 m1 m2 m3);
                     generalize (Category.Morphisms.idtoiso
                                   C0
                                   (ap (p_morphism_of F (s:=_) (d:=_))
                                       (Category.Core.associativity C x1 x2 x3 x4 m1 m2 m3)))
                 | [ |- context[Category.Morphisms.idtoiso
                                     ?C0
                                     (ap (p_morphism_of ?F (s:=_) (d:=_))
                                         (Category.Core.associativity ?C ?x1 ?x2 ?x3 ?x4 ?m1 ?m2 ?m3))] ]
                   => generalize (@p_composition_of_coherent_for_rewrite _ C F x1 x2 x3 x4 m1 m2 m3);
                     generalize (Category.Morphisms.idtoiso
                                   C0
                                   (ap (p_morphism_of F (s:=_) (d:=_))
                                       (Category.Core.associativity C x1 x2 x3 x4 m1 m2 m3)))
               end.
        simpl.
        destruct_head morphism.
        destruct_head object.
        simpl in *.
        repeat match goal with
                 | [ |- context[p_composition_of ?F ?x ?y ?z ?m1 ?m2] ]
                   => generalize dependent (p_composition_of F x y z m1 m2)
                 | [ |- context[p_identity_of ?F ?x] ]
                   => generalize dependent (p_identity_of F x)
                 | [ |- context[p_morphism_of ?F ?x] ]
                   => generalize dependent (p_morphism_of F x)
                 | [ |- context[p_object_of ?F ?x] ]
                   => generalize dependent (p_object_of F x)
               end.
        simpl.
        clear.
        repeat (let H := fresh "x" in intro H).
        repeat match goal with H : _ |- _ => revert H end.
        intro.
>>
*)

    Lemma associativity_helper
          {x x0 : PreCategory} {x1 : Functor x0 x}
          {x2 x3 : PreCategory} {x4 : Functor x3 x2} {x5 x6 : PreCategory}
          {x7 : Functor x6 x5} {x8 x9 : PreCategory} {x10 : Functor x9 x8}
          {x11 : Functor x9 x6} {x12 : Functor x9 x3} {x13 : Functor x0 x6}
          {x14 : Functor x9 x6} {x15 : Functor x8 x5} {x16 : Functor x x5}
          {x17 : Functor x9 x0} {x18 : Functor x8 x}
          {x19 : NaturalTransformation (x18 o x10) (x1 o x17)}
          {x20 : Functor x0 x3} {x21 : Functor x x2}
          {x22 : NaturalTransformation (x21 o x1) (x4 o x20)}
          {x23 : Functor x8 x2} {x24 : Functor x3 x6} {x25 : Functor x2 x5}
          {x26 : NaturalTransformation (x25 o x4) (x7 o x24)}
          {x27 : Functor x8 x5} {x28 : @Isomorphic (_ -> _) x27 (x25 o x23)%functor}
          {x29 : @Isomorphic (_ -> _) x23 (x21 o x18)%functor}
          {x30 : @Isomorphic (_ -> _) x16 (x25 o x21)%functor}
          {x31 : @Isomorphic (_ -> _) x15 (x16 o x18)%functor}
          {x32 : @Isomorphic (_ -> _) x14 (x13 o x17)%functor}
          {x33 : @Isomorphic (_ -> _) x13 (x24 o x20)%functor}
          {x34 : @Isomorphic (_ -> _) x12 (x20 o x17)%functor}
          {x35 : @Isomorphic (_ -> _) x11 (x24 o x12)%functor}
          {x36 : @Isomorphic (_ -> _) x14 x11}
          (x37 : (x36 : Category.Core.morphism _ _ _) =
                 (x35 ^-1
                      o (x24 oL x34 ^-1 o (associator_1 x24 x20 x17 o ((x33 : Category.Core.morphism _ _ _) oR x17 o (x32 : Category.Core.morphism _ _ _)))))%natural_transformation)
          {x38 : @Isomorphic (_ -> _) x15 x27}
          (x39 : x38 ^-1 =
                 (x31 ^-1 o (x30 ^-1 oR x18) o inverse (associator_1 x25 x21 x18)
                      o (x25 oL (x29 : Category.Core.morphism _ _ _)) o (x28 : Category.Core.morphism _ _ _))%natural_transformation)
    : (x7 oL (x36 : Category.Core.morphism _ _ _)
          o (x7 oL x32 ^-1 o associator_1 x7 x13 x17
                o (x7 oL x33 ^-1 o associator_1 x7 x24 x20 o (x26 oR x20)
                      o associator_2 x25 x4 x20 o (x25 oL x22) o
                      associator_1 x25 x21 x1 o ((x30 : Category.Core.morphism _ _ _) oR x1) oR x17)
                o associator_2 x16 x1 x17 o (x16 oL x19) o associator_1 x16 x18 x10
                o ((x31 : Category.Core.morphism _ _ _) oR x10)) o (x38 ^-1 oR x10))%natural_transformation =
      (x7 oL x35 ^-1 o associator_1 x7 x24 x12 o (x26 oR x12)
          o associator_2 x25 x4 x12
          o (x25
               oL (x4 oL x34 ^-1 o associator_1 x4 x20 x17 o (x22 oR x17)
                      o associator_2 x21 x1 x17 o (x21 oL x19)
                      o associator_1 x21 x18 x10 o ((x29 : Category.Core.morphism _ _ _) oR x10)))
          o associator_1 x25 x23 x10 o ((x28 : Category.Core.morphism _ _ _) oR x10))%natural_transformation.H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
x, x0: PreCategory
x1: Functor x0 x
x2, x3: PreCategory
x4: Functor x3 x2
x5, x6: PreCategory
x7: Functor x6 x5
x8, x9: PreCategory
x10: Functor x9 x8
x11: Functor x9 x6
x12: Functor x9 x3
x13: Functor x0 x6
x14: Functor x9 x6
x15: Functor x8 x5
x16: Functor x x5
x17: Functor x9 x0
x18: Functor x8 x
x19: NaturalTransformation (x18 o x10) (x1 o x17)
x20: Functor x0 x3
x21: Functor x x2
x22: NaturalTransformation (x21 o x1) (x4 o x20)
x23: Functor x8 x2
x24: Functor x3 x6
x25: Functor x2 x5
x26: NaturalTransformation (x25 o x4) (x7 o x24)
x27: Functor x8 x5
x28: x27 <~=~> (x25 o x23)%functor
x29: x23 <~=~> (x21 o x18)%functor
x30: x16 <~=~> (x25 o x21)%functor
x31: x15 <~=~> (x16 o x18)%functor
x32: x14 <~=~> (x13 o x17)%functor
x33: x13 <~=~> (x24 o x20)%functor
x34: x12 <~=~> (x20 o x17)%functor
x35: x11 <~=~> (x24 o x12)%functor
x36: x14 <~=~> x11
x37: (x36 : Core.morphism (x9 -> x6) x14 x11) =
(x35^-1
o (x24 oL x34^-1
o (associator_1 x24 x20 x17
o ((x33 : Core.morphism (x0 -> x6) x13 (x24 o x20)%functor) oR x17
o (x32 : Core.morphism (x9 -> x6) x14 (x13 o x17)%functor)))))%natural_transformation
x38: x15 <~=~> x27
x39: x38^-1 =
(x31^-1 o (x30^-1 oR x18) o inverse (associator_1 x25 x21 x18)
o (x25 oL (x29 : Core.morphism (x8 -> x2) x23 (x21 o x18)%functor))
o (x28 : Core.morphism (x8 -> x5) x27 (x25 o x23)%functor))%natural_transformation
(x7 oL (x36 : Core.morphism (x9 -> x6) x14 x11)
 o (x7 oL x32^-1 o associator_1 x7 x13 x17
    o (x7 oL x33^-1 o associator_1 x7 x24 x20
       o (x26 oR x20) o associator_2 x25 x4 x20
       o (x25 oL x22) o associator_1 x25 x21 x1
       o ((x30
           :
           Core.morphism (x -> x5) x16
             (x25 o x21)%functor) oR x1) oR x17)
    o associator_2 x16 x1 x17 o (x16 oL x19)
    o associator_1 x16 x18 x10
    o ((x31
        :
        Core.morphism (x8 -> x5) x15
          (x16 o x18)%functor) oR x10))
 o (x38^-1 oR x10))%natural_transformation =
(x7 oL x35^-1 o associator_1 x7 x24 x12 o (x26 oR x12)
 o associator_2 x25 x4 x12
 o (x25
    oL (x4 oL x34^-1 o associator_1 x4 x20 x17
        o (x22 oR x17) o associator_2 x21 x1 x17
        o (x21 oL x19) o associator_1 x21 x18 x10
        o ((x29
            :
            Core.morphism (x8 -> x2) x23
              (x21 o x18)%functor) oR x10)))
 o associator_1 x25 x23 x10
 o ((x28
     :
     Core.morphism (x8 -> x5) x27 (x25 o x23)%functor)
    oR x10))%natural_transformation
    Proof.H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
x, x0: PreCategory
x1: Functor x0 x
x2, x3: PreCategory
x4: Functor x3 x2
x5, x6: PreCategory
x7: Functor x6 x5
x8, x9: PreCategory
x10: Functor x9 x8
x11: Functor x9 x6
x12: Functor x9 x3
x13: Functor x0 x6
x14: Functor x9 x6
x15: Functor x8 x5
x16: Functor x x5
x17: Functor x9 x0
x18: Functor x8 x
x19: NaturalTransformation (x18 o x10) (x1 o x17)
x20: Functor x0 x3
x21: Functor x x2
x22: NaturalTransformation (x21 o x1) (x4 o x20)
x23: Functor x8 x2
x24: Functor x3 x6
x25: Functor x2 x5
x26: NaturalTransformation (x25 o x4) (x7 o x24)
x27: Functor x8 x5
x28: x27 <~=~> (x25 o x23)%functor
x29: x23 <~=~> (x21 o x18)%functor
x30: x16 <~=~> (x25 o x21)%functor
x31: x15 <~=~> (x16 o x18)%functor
x32: x14 <~=~> (x13 o x17)%functor
x33: x13 <~=~> (x24 o x20)%functor
x34: x12 <~=~> (x20 o x17)%functor
x35: x11 <~=~> (x24 o x12)%functor
x36: x14 <~=~> x11
x37: (x36 : Core.morphism (x9 -> x6) x14 x11) =
(x35^-1
o (x24 oL x34^-1
o (associator_1 x24 x20 x17
o ((x33 : Core.morphism (x0 -> x6) x13 (x24 o x20)%functor) oR x17
o (x32 : Core.morphism (x9 -> x6) x14 (x13 o x17)%functor)))))%natural_transformation
x38: x15 <~=~> x27
x39: x38^-1 =
(x31^-1 o (x30^-1 oR x18) o inverse (associator_1 x25 x21 x18)
o (x25 oL (x29 : Core.morphism (x8 -> x2) x23 (x21 o x18)%functor))
o (x28 : Core.morphism (x8 -> x5) x27 (x25 o x23)%functor))%natural_transformation
(x7 oL (x36 : Core.morphism (x9 -> x6) x14 x11)
 o (x7 oL x32^-1 o associator_1 x7 x13 x17
    o (x7 oL x33^-1 o associator_1 x7 x24 x20
       o (x26 oR x20) o associator_2 x25 x4 x20
       o (x25 oL x22) o associator_1 x25 x21 x1
       o ((x30
           :
           Core.morphism (x -> x5) x16
             (x25 o x21)%functor) oR x1) oR x17)
    o associator_2 x16 x1 x17 o (x16 oL x19)
    o associator_1 x16 x18 x10
    o ((x31
        :
        Core.morphism (x8 -> x5) x15
          (x16 o x18)%functor) oR x10))
 o (x38^-1 oR x10))%natural_transformation =
(x7 oL x35^-1 o associator_1 x7 x24 x12 o (x26 oR x12)
 o associator_2 x25 x4 x12
 o (x25
    oL (x4 oL x34^-1 o associator_1 x4 x20 x17
        o (x22 oR x17) o associator_2 x21 x1 x17
        o (x21 oL x19) o associator_1 x21 x18 x10
        o ((x29
            :
            Core.morphism (x8 -> x2) x23
              (x21 o x18)%functor) oR x10)))
 o associator_1 x25 x23 x10
 o ((x28
     :
     Core.morphism (x8 -> x5) x27 (x25 o x23)%functor)
    oR x10))%natural_transformation
      t. (* 18.647s *)
    Qed.

    Lemma associativity x1 x2 x3 x4
          (m1 : morphism x1 x2) (m2 : morphism x2 x3) (m3 : morphism x3 x4)
    : compose (compose m3 m2) m1 = compose m3 (compose m2 m1).H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
x1, x2, x3, x4: object
m1: morphism x1 x2
m2: morphism x2 x3
m3: morphism x3 x4
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
    Proof.H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
x1, x2, x3, x4: object
m1: morphism x1 x2
m2: morphism x2 x3
m3: morphism x3 x4
compose (compose m3 m2) m1 =
compose m3 (compose m2 m1)
      refine (@path_morphism' _ A B S T _ _
                              (compose (compose m3 m2) m1)
                              (compose m3 (compose m2 m1))
                              (Category.Core.associativity _ _ _ _ _ _ _ _)
                              (Category.Core.associativity _ _ _ _ _ _ _ _)
                              _).H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
x1, x2, x3, x4: object
m1: morphism x1 x2
m2: morphism x2 x3
m3: morphism x3 x4
(f x4
 oL Category.Morphisms.idtoiso (S (a x1) -> S (a x4))
      (ap (p_morphism_of S)
         (Core.associativity A (a x1) (a x2) (a x3)
            (a x4) (g m1) (g m2) (g m3)))
 o p (compose (compose m3 m2) m1)
 o ((Category.Morphisms.idtoiso (T (b x1) -> T (b x4))
       (ap (p_morphism_of T)
          (Core.associativity B (b x1) (b x2) (b x3)
             (b x4) (h m1) (h m2) (h m3))))^-1 oR 
    f x1))%natural_transformation =
p (compose m3 (compose m2 m1))
      simpl.H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
x1, x2, x3, x4: object
m1: morphism x1 x2
m2: morphism x2 x3
m3: morphism x3 x4
(f x4
 oL Category.Morphisms.idtoiso (S (a x1) -> S (a x4))
      (ap (p_morphism_of S)
         (Core.associativity A (a x1) (a x2) (a x3)
            (a x4) (g m1) (g m2) (g m3)))
 o (f x4
    oL (p_composition_of S (a x1) (a x2) (a x4)
          (g m3 o g m2) (g m1))^-1
    o associator_1 (f x4)
        (p_morphism_of S (g m3 o g m2))
        (p_morphism_of S (g m1))
    o (f x4
       oL (p_composition_of S (a x2) (a x3) (a x4)
             (g m3) (g m2))^-1
       o associator_1 (f x4) (p_morphism_of S (g m3))
           (p_morphism_of S (g m2))
       o (p m3 oR p_morphism_of S (g m2))
       o associator_2 (p_morphism_of T (h m3)) (f x3)
           (p_morphism_of S (g m2))
       o (p_morphism_of T (h m3) oL p m2)
       o associator_1 (p_morphism_of T (h m3))
           (p_morphism_of T (h m2)) (f x2)
       o (p_composition_of T (b x2) (b x3) (b x4)
            (h m3) (h m2) oR f x2)
       oR p_morphism_of S (g m1))
    o associator_2 (p_morphism_of T (h m3 o h m2))
        (f x2) (p_morphism_of S (g m1))
    o (p_morphism_of T (h m3 o h m2) oL p m1)
    o associator_1 (p_morphism_of T (h m3 o h m2))
        (p_morphism_of T (h m1)) (f x1)
    o (p_composition_of T (b x1) (b x2) (b x4)
         (h m3 o h m2) (h m1) oR f x1))
 o ((Category.Morphisms.idtoiso (T (b x1) -> T (b x4))
       (ap (p_morphism_of T)
          (Core.associativity B (b x1) (b x2) (b x3)
             (b x4) (h m1) (h m2) (h m3))))^-1 oR 
    f x1))%natural_transformation =
(f x4
 oL (p_composition_of S (a x1) (a x3) (a x4) (g m3)
       (g m2 o g m1))^-1
 o associator_1 (f x4) (p_morphism_of S (g m3))
     (p_morphism_of S (g m2 o g m1))
 o (p m3 oR p_morphism_of S (g m2 o g m1))
 o associator_2 (p_morphism_of T (h m3)) (f x3)
     (p_morphism_of S (g m2 o g m1))
 o (p_morphism_of T (h m3)
    oL (f x3
        oL (p_composition_of S (a x1) (a x2) (a x3)
              (g m2) (g m1))^-1
        o associator_1 (f x3) (p_morphism_of S (g m2))
            (p_morphism_of S (g m1))
        o (p m2 oR p_morphism_of S (g m1))
        o associator_2 (p_morphism_of T (h m2)) (f x2)
            (p_morphism_of S (g m1))
        o (p_morphism_of T (h m2) oL p m1)
        o associator_1 (p_morphism_of T (h m2))
            (p_morphism_of T (h m1)) (f x1)
        o (p_composition_of T (b x1) (b x2) (b x3)
             (h m2) (h m1) oR f x1)))
 o associator_1 (p_morphism_of T (h m3))
     (p_morphism_of T (h m2 o h m1)) (f x1)
 o (p_composition_of T (b x1) (b x3) (b x4) (h m3)
      (h m2 o h m1) oR f x1))%natural_transformation
      apply associativity_helper.H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
x1, x2, x3, x4: object
m1: morphism x1 x2
m2: morphism x2 x3
m3: morphism x3 x4
Category.Morphisms.idtoiso (S (a x1) -> S (a x4))
  (ap (p_morphism_of S)
     (Core.associativity A (a x1) (a x2) (a x3) (a x4)
        (g m1) (g m2) (g m3))) =
((p_composition_of S (a x1) (a x3) (a x4) (g m3)
    (g m2 o g m1))^-1
 o (p_morphism_of S (g m3)
    oL (p_composition_of S (a x1) (a x2) (a x3) (g m2)
          (g m1))^-1
    o (associator_1 (p_morphism_of S (g m3))
         (p_morphism_of S (g m2))
         (p_morphism_of S (g m1))
       o (p_composition_of S (a x2) (a x3) (a x4)
            (g m3) (g m2) oR p_morphism_of S (g m1)
          o p_composition_of S (a x1) (a x2) (a x4)
              (g m3 o g m2) (g m1)))))%natural_transformation
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
x1, x2, x3, x4: object
m1: morphism x1 x2
m2: morphism x2 x3
m3: morphism x3 x4
(Category.Morphisms.idtoiso (T (b x1) -> T (b x4))
   (ap (p_morphism_of T)
      (Core.associativity B (b x1) (b x2) (b x3)
         (b x4) (h m1) (h m2) (h m3))))^-1 =
((p_composition_of T (b x1) (b x2) (b x4)
    (h m3 o h m2) (h m1))^-1
 o ((p_composition_of T (b x2) (b x3) (b x4) (h m3)
       (h m2))^-1 oR p_morphism_of T (h m1))
 o inverse
     (associator_1 (p_morphism_of T (h m3))
        (p_morphism_of T (h m2))
        (p_morphism_of T (h m1)))
 o (p_morphism_of T (h m3)
    oL p_composition_of T (b x1) (b x2) (b x3) (h m2)
         (h m1))
 o p_composition_of T (b x1) (b x3) (b x4) (h m3)
     (h m2 o h m1))%natural_transformation
      -H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
x1, x2, x3, x4: object
m1: morphism x1 x2
m2: morphism x2 x3
m3: morphism x3 x4
Category.Morphisms.idtoiso (S (a x1) -> S (a x4))
  (ap (p_morphism_of S)
     (Core.associativity A (a x1) (a x2) (a x3) (a x4)
        (g m1) (g m2) (g m3))) =
((p_composition_of S (a x1) (a x3) (a x4) (g m3)
    (g m2 o g m1))^-1
 o (p_morphism_of S (g m3)
    oL (p_composition_of S (a x1) (a x2) (a x3) (g m2)
          (g m1))^-1
    o (associator_1 (p_morphism_of S (g m3))
         (p_morphism_of S (g m2))
         (p_morphism_of S (g m1))
       o (p_composition_of S (a x2) (a x3) (a x4)
            (g m3) (g m2) oR p_morphism_of S (g m1)
          o p_composition_of S (a x1) (a x2) (a x4)
              (g m3 o g m2) (g m1)))))%natural_transformation exact (p_composition_of_coherent_for_rewrite _ _ _ _ _ _ _ _).
      -H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
x1, x2, x3, x4: object
m1: morphism x1 x2
m2: morphism x2 x3
m3: morphism x3 x4
(Category.Morphisms.idtoiso (T (b x1) -> T (b x4))
   (ap (p_morphism_of T)
      (Core.associativity B (b x1) (b x2) (b x3)
         (b x4) (h m1) (h m2) (h m3))))^-1 =
((p_composition_of T (b x1) (b x2) (b x4)
    (h m3 o h m2) (h m1))^-1
 o ((p_composition_of T (b x2) (b x3) (b x4) (h m3)
       (h m2))^-1 oR p_morphism_of T (h m1))
 o inverse
     (associator_1 (p_morphism_of T (h m3))
        (p_morphism_of T (h m2))
        (p_morphism_of T (h m1)))
 o (p_morphism_of T (h m3)
    oL p_composition_of T (b x1) (b x2) (b x3) (h m2)
         (h m1))
 o p_composition_of T (b x1) (b x3) (b x4) (h m3)
     (h m2 o h m1))%natural_transformation exact (p_composition_of_coherent_inverse_for_rewrite _ _ _ _ _ _ _ _).
    Defined.

    (** Ugh.  To construct the type of this lemma, the code is:
<<
Lemma left_identity (s d : object) (m : morphism s d)
      : compose (identity _) m = m.
      Proof.
        exact (@path_morphism' _ _
                               (compose (identity _) m) m
                               (Category.Core.left_identity _ _ _ _)
                               (Category.Core.left_identity _ _ _ _)
                               _).
        simpl in *.
        repeat match goal with
                 | [ |- context[@morphism_inverse
                                     _ _ _ _
                                     (@isisomorphism_isomorphic
                                        _ _ _
                                        (Category.Morphisms.idtoiso
                                           ?C0
                                           (ap (p_morphism_of ?F (s:=_) (d:=_))
                                               (Category.Core.left_identity ?C ?x ?y ?f))))] ]
                   => generalize (@p_left_identity_of_coherent_inverse_for_rewrite _ C F x y f);
                     generalize (Category.Morphisms.idtoiso
                                   C0
                                   (ap (p_morphism_of F (s:=_) (d:=_))
                                       (Category.Core.left_identity C x y f)))
                 | [ |- context[Category.Morphisms.idtoiso
                                     ?C0
                                     (ap (p_morphism_of ?F (s:=_) (d:=_))
                                         (Category.Core.left_identity ?C ?x ?y ?f))] ]
                   => generalize (@p_left_identity_of_coherent_for_rewrite _ C F x y f);
                     generalize (Category.Morphisms.idtoiso
                                   C0
                                   (ap (p_morphism_of F (s:=_) (d:=_))
                                       (Category.Core.left_identity C x y f)))
               end.
        simpl.
        destruct_head morphism.
        destruct_head object.
        simpl in *.
        repeat match goal with
                 | [ |- context[p_composition_of ?F ?x ?y ?z ?m1 ?m2] ]
                   => generalize dependent (p_composition_of F x y z m1 m2)
                 | [ |- context[p_identity_of ?F ?x] ]
                   => generalize dependent (p_identity_of F x)
                 | [ |- context[p_morphism_of ?F ?x] ]
                   => generalize dependent (p_morphism_of F x)
                 | [ |- context[p_object_of ?F ?x] ]
                   => generalize dependent (p_object_of F x)
               end.
        simpl.
        clear.
        repeat (let H := fresh "x" in intro H).
        repeat match goal with H : _ |- _ => revert H end.
        intro.
>>
*)

    Lemma left_identity_helper
          {x x0 : PreCategory} {x1 : Functor x0 x}
          {x2 x3 : PreCategory} {x4 : Functor x3 x2} {x5 x6 : Functor x3 x0}
          {x7 : Functor x2 x} {x8 : NaturalTransformation (x7 o x4) (x1 o x6)}
          {x9 : Functor x2 x} {x10 : Functor x0 x0} {x11 : Functor x x}
          {x12 : @Isomorphic (_ -> _) x11 1%functor} {x13 : @Isomorphic (_ -> _) x10 1%functor}
          {x14 : @Isomorphic (_ -> _) x9 (x11 o x7)%functor} {x15 : @Isomorphic (_ -> _) x5 (x10 o x6)%functor}
          {x16 : @Isomorphic (_ -> _) x5 x6}
          {x17 : (x16 : Category.Core.morphism _ _ _) =
                 (left_identity_natural_transformation_1 x6 o ((x13 : Category.Core.morphism _ _ _) oR x6 o (x15 : Category.Core.morphism _ _ _)))%natural_transformation}
          {x18 : @Isomorphic (_ -> _) x9 x7}
          {x19 : x18 ^-1 =
                 (x14 ^-1 o (x12 ^-1 oR x7)
                      o inverse (left_identity_natural_transformation_1 x7))%natural_transformation}
    : (x1 oL (x16 : Category.Core.morphism _ _ _)
          o (x1 oL x15 ^-1 o associator_1 x1 x10 x6
                o (x1 oL x13 ^-1 o right_identity_natural_transformation_2 x1
                      o left_identity_natural_transformation_1 x1 o
                      ((x12 : Category.Core.morphism _ _ _) oR x1) oR x6) o associator_2 x11 x1 x6 o
                (x11 oL x8) o associator_1 x11 x7 x4 o ((x14 : Category.Core.morphism _ _ _) oR x4)) o
          (x18 ^-1 oR x4))%natural_transformation = x8.H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
x, x0: PreCategory
x1: Functor x0 x
x2, x3: PreCategory
x4: Functor x3 x2
x5, x6: Functor x3 x0
x7: Functor x2 x
x8: NaturalTransformation (x7 o x4) (x1 o x6)
x9: Functor x2 x
x10: Functor x0 x0
x11: Functor x x
x12: x11 <~=~> 1%functor
x13: x10 <~=~> 1%functor
x14: x9 <~=~> (x11 o x7)%functor
x15: x5 <~=~> (x10 o x6)%functor
x16: x5 <~=~> x6
x17: (x16 : Core.morphism (x3 -> x0) x5 x6) =
(left_identity_natural_transformation_1 x6
o ((x13 : Core.morphism (x0 -> x0) x10 1%functor) oR x6
o (x15 : Core.morphism (x3 -> x0) x5 (x10 o x6)%functor)))%natural_transformation
x18: x9 <~=~> x7
x19: x18^-1 =
(x14^-1 o (x12^-1 oR x7)
o inverse (left_identity_natural_transformation_1 x7))%natural_transformation
(x1 oL (x16 : Core.morphism (x3 -> x0) x5 x6)
 o (x1 oL x15^-1 o associator_1 x1 x10 x6
    o (x1 oL x13^-1
       o right_identity_natural_transformation_2 x1
       o left_identity_natural_transformation_1 x1
       o ((x12 : Core.morphism (x -> x) x11 1%functor)
          oR x1) oR x6) o associator_2 x11 x1 x6
    o (x11 oL x8) o associator_1 x11 x7 x4
    o ((x14
        :
        Core.morphism (x2 -> x) x9 (x11 o x7)%functor)
       oR x4)) o (x18^-1 oR x4))%natural_transformation =
x8
    Proof.H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
x, x0: PreCategory
x1: Functor x0 x
x2, x3: PreCategory
x4: Functor x3 x2
x5, x6: Functor x3 x0
x7: Functor x2 x
x8: NaturalTransformation (x7 o x4) (x1 o x6)
x9: Functor x2 x
x10: Functor x0 x0
x11: Functor x x
x12: x11 <~=~> 1%functor
x13: x10 <~=~> 1%functor
x14: x9 <~=~> (x11 o x7)%functor
x15: x5 <~=~> (x10 o x6)%functor
x16: x5 <~=~> x6
x17: (x16 : Core.morphism (x3 -> x0) x5 x6) =
(left_identity_natural_transformation_1 x6
o ((x13 : Core.morphism (x0 -> x0) x10 1%functor) oR x6
o (x15 : Core.morphism (x3 -> x0) x5 (x10 o x6)%functor)))%natural_transformation
x18: x9 <~=~> x7
x19: x18^-1 =
(x14^-1 o (x12^-1 oR x7)
o inverse (left_identity_natural_transformation_1 x7))%natural_transformation
(x1 oL (x16 : Core.morphism (x3 -> x0) x5 x6)
 o (x1 oL x15^-1 o associator_1 x1 x10 x6
    o (x1 oL x13^-1
       o right_identity_natural_transformation_2 x1
       o left_identity_natural_transformation_1 x1
       o ((x12 : Core.morphism (x -> x) x11 1%functor)
          oR x1) oR x6) o associator_2 x11 x1 x6
    o (x11 oL x8) o associator_1 x11 x7 x4
    o ((x14
        :
        Core.morphism (x2 -> x) x9 (x11 o x7)%functor)
       oR x4)) o (x18^-1 oR x4))%natural_transformation =
x8
      t. (* 3.959 s *)
    Qed.

    Lemma left_identity (s d : object) (m : morphism s d)
    : compose (identity _) m = m.H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
s, d: object
m: morphism s d
compose (identity d) m = m
    Proof.H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
s, d: object
m: morphism s d
compose (identity d) m = m
      refine (@path_morphism' _ A B S T _ _
                              (compose (identity _) m) m
                              (Category.Core.left_identity _ _ _ _)
                              (Category.Core.left_identity _ _ _ _)
                              _).H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
s, d: object
m: morphism s d
(f d
 oL Category.Morphisms.idtoiso (S (a s) -> S (a d))
      (ap (p_morphism_of S)
         (Core.left_identity A (a s) (a d) (g m)))
 o p (compose (identity d) m)
 o ((Category.Morphisms.idtoiso (T (b s) -> T (b d))
       (ap (p_morphism_of T)
          (Core.left_identity B (b s) (b d) (h m))))^-1
    oR f s))%natural_transformation = p m
      simpl.H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
s, d: object
m: morphism s d
(f d
 oL Category.Morphisms.idtoiso (S (a s) -> S (a d))
      (ap (p_morphism_of S)
         (Core.left_identity A (a s) (a d) (g m)))
 o (f d
    oL (p_composition_of S (a s) (a d) (a d) 1 (g m))^-1
    o associator_1 (f d) (p_morphism_of S 1)
        (p_morphism_of S (g m))
    o (f d oL (p_identity_of S (a d))^-1
       o right_identity_natural_transformation_2 (f d)
       o left_identity_natural_transformation_1 (f d)
       o (p_identity_of T (b d) oR f d)
       oR p_morphism_of S (g m))
    o associator_2 (p_morphism_of T 1) (f d)
        (p_morphism_of S (g m))
    o (p_morphism_of T 1 oL p m)
    o associator_1 (p_morphism_of T 1)
        (p_morphism_of T (h m)) (f s)
    o (p_composition_of T (b s) (b d) (b d) 1 (h m)
       oR f s))
 o ((Category.Morphisms.idtoiso (T (b s) -> T (b d))
       (ap (p_morphism_of T)
          (Core.left_identity B (b s) (b d) (h m))))^-1
    oR f s))%natural_transformation = p m
      refine left_identity_helper.H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
s, d: object
m: morphism s d
Category.Morphisms.idtoiso (S (a s) -> S (a d))
  (ap (p_morphism_of S)
     (Core.left_identity A (a s) (a d) (g m))) =
(left_identity_natural_transformation_1
   (p_morphism_of S (g m))
 o (p_identity_of S (a d) oR p_morphism_of S (g m)
    o p_composition_of S (a s) (a d) (a d) 1 (g m)))%natural_transformation
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
s, d: object
m: morphism s d
(Category.Morphisms.idtoiso (T (b s) -> T (b d))
   (ap (p_morphism_of T)
      (Core.left_identity B (b s) (b d) (h m))))^-1 =
((p_composition_of T (b s) (b d) (b d) 1 (h m))^-1
 o ((p_identity_of T (b d))^-1
    oR p_morphism_of T (h m))
 o inverse
     (left_identity_natural_transformation_1
        (p_morphism_of T (h m))))%natural_transformation
      -H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
s, d: object
m: morphism s d
Category.Morphisms.idtoiso (S (a s) -> S (a d))
  (ap (p_morphism_of S)
     (Core.left_identity A (a s) (a d) (g m))) =
(left_identity_natural_transformation_1
   (p_morphism_of S (g m))
 o (p_identity_of S (a d) oR p_morphism_of S (g m)
    o p_composition_of S (a s) (a d) (a d) 1 (g m)))%natural_transformation exact (p_left_identity_of_coherent_for_rewrite _ _ _ _).
      -H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
s, d: object
m: morphism s d
(Category.Morphisms.idtoiso (T (b s) -> T (b d))
   (ap (p_morphism_of T)
      (Core.left_identity B (b s) (b d) (h m))))^-1 =
((p_composition_of T (b s) (b d) (b d) 1 (h m))^-1
 o ((p_identity_of T (b d))^-1
    oR p_morphism_of T (h m))
 o inverse
     (left_identity_natural_transformation_1
        (p_morphism_of T (h m))))%natural_transformation exact (p_left_identity_of_coherent_inverse_for_rewrite _ _ _ _).
    Defined.

    (** To generate the type of this helper lemma, we used:
<<
      Lemma right_identity (s d : object) (m : morphism s d)
      : compose m (identity _) = m.
      Proof.
        exact (@path_morphism' _ _
                               (compose m (identity _)) m
                               (Category.Core.right_identity _ _ _ _)
                               (Category.Core.right_identity _ _ _ _)
                               _).
        simpl in *.
        repeat match goal with
                 | [ |- context[@morphism_inverse
                                     _ _ _ _
                                     (@isisomorphism_isomorphic
                                        _ _ _
                                        (Category.Morphisms.idtoiso
                                           ?C0
                                           (ap (p_morphism_of ?F (s:=_) (d:=_))
                                               (Category.Core.right_identity ?C ?x ?y ?f))))] ]
                   => generalize (@p_right_identity_of_coherent_inverse_for_rewrite _ C F x y f);
                     generalize (Category.Morphisms.idtoiso
                                   C0
                                   (ap (p_morphism_of F (s:=_) (d:=_))
                                       (Category.Core.right_identity C x y f)))
                 | [ |- context[Category.Morphisms.idtoiso
                                     ?C0
                                     (ap (p_morphism_of ?F (s:=_) (d:=_))
                                         (Category.Core.right_identity ?C ?x ?y ?f))] ]
                   => generalize (@p_right_identity_of_coherent_for_rewrite _ C F x y f);
                     generalize (Category.Morphisms.idtoiso
                                   C0
                                   (ap (p_morphism_of F (s:=_) (d:=_))
                                       (Category.Core.right_identity C x y f)))
               end.
        simpl.
        destruct_head morphism.
        destruct_head object.
        simpl in *.
        repeat match goal with
                 | [ |- context[p_composition_of ?F ?x ?y ?z ?m1 ?m2] ]
                   => generalize dependent (p_composition_of F x y z m1 m2)
                 | [ |- context[p_identity_of ?F ?x] ]
                   => generalize dependent (p_identity_of F x)
                 | [ |- context[p_morphism_of ?F ?x] ]
                   => generalize dependent (p_morphism_of F x)
                 | [ |- context[p_object_of ?F ?x] ]
                   => generalize dependent (p_object_of F x)
               end.
        simpl.
        clear.
        repeat (let H := fresh "x" in intro H).
        repeat match goal with H : _ |- _ => revert H end.
        intro.
>>
*)

    Lemma right_identity_helper
          {x x0 : PreCategory} {x1 : Functor x0 x}
          {x2 x3 : PreCategory} {x4 : Functor x3 x2} {x5 x6 : Functor x3 x0}
          {x7 : Functor x2 x} {x8 : NaturalTransformation (x7 o x4) (x1 o x6)}
          {x9 : Functor x2 x} {x10 : Functor x3 x3} {x11 : Functor x2 x2}
          {x12 : @Isomorphic (_ -> _) x11 1%functor} {x13 : @Isomorphic (_ -> _) x10 1%functor}
          {x14 : @Isomorphic (_ -> _) x9 (x7 o x11)%functor} {x15 : @Isomorphic (_ -> _) x5 (x6 o x10)%functor}
          {x16 : @Isomorphic (_ -> _) x5 x6}
          {x17 : (x16 : Category.Core.morphism _ _ _) =
                 (right_identity_natural_transformation_1 x6 o (x6 oL (x13 : Category.Core.morphism _ _ _) o (x15 : Category.Core.morphism _ _ _)))%natural_transformation}
          {x18 : @Isomorphic (_ -> _) x9 x7}
          {x19 : x18 ^-1 =
                 (x14 ^-1 o (x7 oL x12 ^-1)
                      o inverse (right_identity_natural_transformation_1 x7))%natural_transformation}
    : (x1 oL (x16 : Category.Core.morphism _ _ _)
          o (x1 oL x15 ^-1 o associator_1 x1 x6 x10 o (x8 oR x10)
                o associator_2 x7 x4 x10
                o (x7
                     oL (x4 oL x13 ^-1 o right_identity_natural_transformation_2 x4
                            o left_identity_natural_transformation_1 x4 o
                            ((x12 : Category.Core.morphism _ _ _) oR x4))) o associator_1 x7 x11 x4 o
                ((x14 : Category.Core.morphism _ _ _) oR x4)) o (x18 ^-1 oR x4))%natural_transformation = x8.H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
x, x0: PreCategory
x1: Functor x0 x
x2, x3: PreCategory
x4: Functor x3 x2
x5, x6: Functor x3 x0
x7: Functor x2 x
x8: NaturalTransformation (x7 o x4) (x1 o x6)
x9: Functor x2 x
x10: Functor x3 x3
x11: Functor x2 x2
x12: x11 <~=~> 1%functor
x13: x10 <~=~> 1%functor
x14: x9 <~=~> (x7 o x11)%functor
x15: x5 <~=~> (x6 o x10)%functor
x16: x5 <~=~> x6
x17: (x16 : Core.morphism (x3 -> x0) x5 x6) =
(right_identity_natural_transformation_1 x6
o (x6 oL (x13 : Core.morphism (x3 -> x3) x10 1%functor)
o (x15 : Core.morphism (x3 -> x0) x5 (x6 o x10)%functor)))%natural_transformation
x18: x9 <~=~> x7
x19: x18^-1 =
(x14^-1 o (x7 oL x12^-1)
o inverse (right_identity_natural_transformation_1 x7))%natural_transformation
(x1 oL (x16 : Core.morphism (x3 -> x0) x5 x6)
 o (x1 oL x15^-1 o associator_1 x1 x6 x10
    o (x8 oR x10) o associator_2 x7 x4 x10
    o (x7
       oL (x4 oL x13^-1
           o right_identity_natural_transformation_2
               x4
           o left_identity_natural_transformation_1 x4
           o ((x12
               :
               Core.morphism (x2 -> x2) x11 1%functor)
              oR x4))) o associator_1 x7 x11 x4
    o ((x14
        :
        Core.morphism (x2 -> x) x9 (x7 o x11)%functor)
       oR x4)) o (x18^-1 oR x4))%natural_transformation =
x8
    Proof.H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
x, x0: PreCategory
x1: Functor x0 x
x2, x3: PreCategory
x4: Functor x3 x2
x5, x6: Functor x3 x0
x7: Functor x2 x
x8: NaturalTransformation (x7 o x4) (x1 o x6)
x9: Functor x2 x
x10: Functor x3 x3
x11: Functor x2 x2
x12: x11 <~=~> 1%functor
x13: x10 <~=~> 1%functor
x14: x9 <~=~> (x7 o x11)%functor
x15: x5 <~=~> (x6 o x10)%functor
x16: x5 <~=~> x6
x17: (x16 : Core.morphism (x3 -> x0) x5 x6) =
(right_identity_natural_transformation_1 x6
o (x6 oL (x13 : Core.morphism (x3 -> x3) x10 1%functor)
o (x15 : Core.morphism (x3 -> x0) x5 (x6 o x10)%functor)))%natural_transformation
x18: x9 <~=~> x7
x19: x18^-1 =
(x14^-1 o (x7 oL x12^-1)
o inverse (right_identity_natural_transformation_1 x7))%natural_transformation
(x1 oL (x16 : Core.morphism (x3 -> x0) x5 x6)
 o (x1 oL x15^-1 o associator_1 x1 x6 x10
    o (x8 oR x10) o associator_2 x7 x4 x10
    o (x7
       oL (x4 oL x13^-1
           o right_identity_natural_transformation_2
               x4
           o left_identity_natural_transformation_1 x4
           o ((x12
               :
               Core.morphism (x2 -> x2) x11 1%functor)
              oR x4))) o associator_1 x7 x11 x4
    o ((x14
        :
        Core.morphism (x2 -> x) x9 (x7 o x11)%functor)
       oR x4)) o (x18^-1 oR x4))%natural_transformation =
x8
      t. (* 3.26 s *)
    Qed.

    Lemma right_identity (s d : object) (m : morphism s d)
    : compose m (identity _) = m.H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
s, d: object
m: morphism s d
compose m (identity s) = m
    Proof.H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
s, d: object
m: morphism s d
compose m (identity s) = m
      refine (@path_morphism' _ A B S T _ _
                              (compose m (identity _)) m
                              (Category.Core.right_identity _ _ _ _)
                              (Category.Core.right_identity _ _ _ _)
                              _).H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
s, d: object
m: morphism s d
(f d
 oL Category.Morphisms.idtoiso (S (a s) -> S (a d))
      (ap (p_morphism_of S)
         (Core.right_identity A (a s) (a d) (g m)))
 o p (compose m (identity s))
 o ((Category.Morphisms.idtoiso (T (b s) -> T (b d))
       (ap (p_morphism_of T)
          (Core.right_identity B (b s) (b d) (h m))))^-1
    oR f s))%natural_transformation = p m
      simpl.H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
s, d: object
m: morphism s d
(f d
 oL Category.Morphisms.idtoiso (S (a s) -> S (a d))
      (ap (p_morphism_of S)
         (Core.right_identity A (a s) (a d) (g m)))
 o (f d
    oL (p_composition_of S (a s) (a s) (a d) (g m) 1)^-1
    o associator_1 (f d) (p_morphism_of S (g m))
        (p_morphism_of S 1)
    o (p m oR p_morphism_of S 1)
    o associator_2 (p_morphism_of T (h m)) (f s)
        (p_morphism_of S 1)
    o (p_morphism_of T (h m)
       oL (f s oL (p_identity_of S (a s))^-1
           o right_identity_natural_transformation_2
               (f s)
           o left_identity_natural_transformation_1
               (f s) o (p_identity_of T (b s) oR f s)))
    o associator_1 (p_morphism_of T (h m))
        (p_morphism_of T 1) (f s)
    o (p_composition_of T (b s) (b s) (b d) (h m) 1
       oR f s))
 o ((Category.Morphisms.idtoiso (T (b s) -> T (b d))
       (ap (p_morphism_of T)
          (Core.right_identity B (b s) (b d) (h m))))^-1
    oR f s))%natural_transformation = p m
      refine right_identity_helper.H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
s, d: object
m: morphism s d
Category.Morphisms.idtoiso (S (a s) -> S (a d))
  (ap (p_morphism_of S)
     (Core.right_identity A (a s) (a d) (g m))) =
(right_identity_natural_transformation_1
   (p_morphism_of S (g m))
 o (p_morphism_of S (g m) oL p_identity_of S (a s)
    o p_composition_of S (a s) (a s) (a d) (g m) 1))%natural_transformation
H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
s, d: object
m: morphism s d
(Category.Morphisms.idtoiso (T (b s) -> T (b d))
   (ap (p_morphism_of T)
      (Core.right_identity B (b s) (b d) (h m))))^-1 =
((p_composition_of T (b s) (b s) (b d) (h m) 1)^-1
 o (p_morphism_of T (h m)
    oL (p_identity_of T (b s))^-1)
 o inverse
     (right_identity_natural_transformation_1
        (p_morphism_of T (h m))))%natural_transformation
      -H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
s, d: object
m: morphism s d
Category.Morphisms.idtoiso (S (a s) -> S (a d))
  (ap (p_morphism_of S)
     (Core.right_identity A (a s) (a d) (g m))) =
(right_identity_natural_transformation_1
   (p_morphism_of S (g m))
 o (p_morphism_of S (g m) oL p_identity_of S (a s)
    o p_composition_of S (a s) (a s) (a d) (g m) 1))%natural_transformation exact (p_right_identity_of_coherent_for_rewrite _ _ _ _).
      -H: Funext
A, B: PreCategory
S: Pseudofunctor A
T: Pseudofunctor B
H0: forall (a : A) (b : B),
IsHSet (Functor (S a) (T b))
s, d: object
m: morphism s d
(Category.Morphisms.idtoiso (T (b s) -> T (b d))
   (ap (p_morphism_of T)
      (Core.right_identity B (b s) (b d) (h m))))^-1 =
((p_composition_of T (b s) (b s) (b d) (h m) 1)^-1
 o (p_morphism_of T (h m)
    oL (p_identity_of T (b s))^-1)
 o inverse
     (right_identity_natural_transformation_1
        (p_morphism_of T (h m))))%natural_transformation exact (p_right_identity_of_coherent_inverse_for_rewrite _ _ _ _).
    Defined.
  End lax_comma_category_parts.
End LaxCommaCategory.