RewriteLaws.v

(** * Pseudofunctor rewriting helper lemmas *)
Require Import Category.Core Functor.Core NaturalTransformation.Core.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Category.Morphisms FunctorCategory.Morphisms.
Require Import Functor.Composition.Core.
Require Import NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws.
Require Import NaturalTransformation.Isomorphisms.
Require Import NaturalTransformation.Paths.
Require Import FunctorCategory.Core.
Require Import Pseudofunctor.Core.
Require Import HoTT.Tactics.

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

Local Open Scope morphism_scope.

Section lemmas.
  Local Open Scope natural_transformation_scope.
  Context `{Funext}.

  Variable C : PreCategory.
  Variable F : Pseudofunctor C.

  Lemma p_composition_of_coherent_for_rewrite_helper w x y z
        (f : morphism C w x) (g : morphism C x y) (h : morphism C y z)
        (p p0 p1 p2 : PreCategory) (f0 : morphism C w z -> Functor p2 p1)
        (f1 : Functor p0 p1) (f2 : Functor p2 p) (f3 : Functor p p0)
        (f4 : Functor p2 p0) `(@IsIsomorphism (_ -> _) f4 (f3 o f2)%functor n)
        `(@IsIsomorphism (_ -> _) (f0 (h o (g o f))%morphism) (f1 o f4)%functor n0)
  : @paths (NaturalTransformation _ _)
           (@morphism_isomorphic _ _ _ (Category.Morphisms.idtoiso (p2 -> p1) (ap f0 (Category.Core.associativity C w x y z f g h))))
           (n0^-1
              o ((f1 oL n^-1)
                   o ((f1 oL n)
                        o (n0
                             o (@morphism_isomorphic _ _ _ (Category.Morphisms.idtoiso (p2 -> p1) (ap f0 (Category.Core.associativity C w x y z f g h))))))))%natural_transformation.H: Funext
C: PreCategory
F: Pseudofunctor C
w, x, y, z: C
f: morphism C w x
g: morphism C x y
h: morphism C y z
p, p0, p1, p2: PreCategory
f0: morphism C w z -> Functor p2 p1
f1: Functor p0 p1
f2: Functor p2 p
f3: Functor p p0
f4: Functor p2 p0
n: morphism (p2 -> p0) f4 (f3 o f2)%functor
H0: IsIsomorphism n
n0: morphism (p2 -> p1) (f0 (h o (g o f))%morphism)
  (f1 o f4)%functor
H1: IsIsomorphism n0
Category.Morphisms.idtoiso (p2 -> p1)
  (ap f0 (Core.associativity C w x y z f g h)) =
n0^-1
o (f1 oL n^-1
   o (f1 oL n
      o (n0
         o Category.Morphisms.idtoiso (p2 -> p1)
             (ap f0
                (Core.associativity C w x y z f g h)))))
  Proof.H: Funext
C: PreCategory
F: Pseudofunctor C
w, x, y, z: C
f: morphism C w x
g: morphism C x y
h: morphism C y z
p, p0, p1, p2: PreCategory
f0: morphism C w z -> Functor p2 p1
f1: Functor p0 p1
f2: Functor p2 p
f3: Functor p p0
f4: Functor p2 p0
n: morphism (p2 -> p0) f4 (f3 o f2)%functor
H0: IsIsomorphism n
n0: morphism (p2 -> p1) (f0 (h o (g o f))%morphism)
  (f1 o f4)%functor
H1: IsIsomorphism n0
Category.Morphisms.idtoiso (p2 -> p1)
  (ap f0 (Core.associativity C w x y z f g h)) =
n0^-1
o (f1 oL n^-1
   o (f1 oL n
      o (n0
         o Category.Morphisms.idtoiso (p2 -> p1)
             (ap f0
                (Core.associativity C w x y z f g h)))))
    simpl in *.H: Funext
C: PreCategory
F: Pseudofunctor C
w, x, y, z: C
f: morphism C w x
g: morphism C x y
h: morphism C y z
p, p0, p1, p2: PreCategory
f0: morphism C w z -> Functor p2 p1
f1: Functor p0 p1
f2: Functor p2 p
f3: Functor p p0
f4: Functor p2 p0
n: NaturalTransformation f4 (f3 o f2)
H0: IsIsomorphism n
n0: NaturalTransformation (f0 (h o (g o f))%morphism)
  (f1 o f4)
H1: IsIsomorphism n0
Category.Morphisms.idtoiso (p2 -> p1)
  (ap f0 (Core.associativity C w x y z f g h)) =
n0^-1
o (f1 oL n^-1
   o (f1 oL n
      o (n0
         o Category.Morphisms.idtoiso (p2 -> p1)
             (ap f0
                (Core.associativity C w x y z f g h)))))
    let C := match goal with |- @paths (@NaturalTransformation ?C ?D ?F ?G) _ _ => constr:((C -> D)%category) end in
    apply (@iso_moveL_Vp C);
      apply (@iso_moveL_Mp C _ _ _ _ _ _ (iso_whisker_l _ _ _ _ _ _ _)).H: Funext
C: PreCategory
F: Pseudofunctor C
w, x, y, z: C
f: morphism C w x
g: morphism C x y
h: morphism C y z
p, p0, p1, p2: PreCategory
f0: morphism C w z -> Functor p2 p1
f1: Functor p0 p1
f2: Functor p2 p
f3: Functor p p0
f4: Functor p2 p0
n: NaturalTransformation f4 (f3 o f2)
H0: IsIsomorphism n
n0: NaturalTransformation (f0 (h o (g o f))%morphism)
  (f1 o f4)
H1: IsIsomorphism n0
((f1 oL n^-1)^-1
 o (n0
    o Category.Morphisms.idtoiso (p2 -> p1)
        (ap f0 (Core.associativity C w x y z f g h))))%morphism =
f1 oL n
o (n0
   o Category.Morphisms.idtoiso (p2 -> p1)
       (ap f0 (Core.associativity C w x y z f g h)))
    path_natural_transformation.H: Funext
C: PreCategory
F: Pseudofunctor C
w, x, y, z: C
f: morphism C w x
g: morphism C x y
h: morphism C y z
p, p0, p1, p2: PreCategory
f0: morphism C w z -> Functor p2 p1
f1: Functor p0 p1
f2: Functor p2 p
f3: Functor p p0
f4: Functor p2 p0
n: NaturalTransformation f4 (f3 o f2)
H0: IsIsomorphism n
n0: NaturalTransformation (f0 (h o (g o f))%morphism)
  (f1 o f4)
H1: IsIsomorphism n0
x0: p2
(f1 _1 (n x0)
 o (n0 x0
    o Category.Morphisms.idtoiso (p2 -> p1)
        (ap f0 (Core.associativity C w x y z f g h))
        x0))%morphism =
(f1 _1 (n x0)
 o (n0 x0
    o Category.Morphisms.idtoiso (p2 -> p1)
        (ap f0 (Core.associativity C w x y z f g h))
        x0))%morphism
    reflexivity.
  Qed.

  Arguments p_composition_of_coherent_for_rewrite_helper {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _}.

  Section helper.
    Context
      {w x y z}
      {f : Functor (F w) (F z)} {f0 : Functor (F w) (F y)}
      {f1 : Functor (F x) (F y)} {f2 : Functor (F y) (F z)}
      {f3 : Functor (F w) (F x)} {f4 : Functor (F x) (F z)}
      {f5 : Functor (F w) (F z)} {n : f5 <~=~> (f4 o f3)%functor}
      {n0 : f4 <~=~> (f2 o f1)%functor} {n1 : f0 <~=~> (f1 o f3)%functor}
      {n2 : f <~=~> (f2 o f0)%functor}.

    Lemma p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper'
    : @IsIsomorphism
        (_ -> _) _ _
        (n2 ^-1 o (f2 oL n1 ^-1 o (associator_1 f2 f1 f3 o (n0 oR f3 o n))))%natural_transformation.H: Funext
C: PreCategory
F: Pseudofunctor C
w, x, y, z: C
f: Functor (F w) (F z)
f0: Functor (F w) (F y)
f1: Functor (F x) (F y)
f2: Functor (F y) (F z)
f3: Functor (F w) (F x)
f4: Functor (F x) (F z)
f5: Functor (F w) (F z)
n: f5 <~=~> (f4 o f3)%functor
n0: f4 <~=~> (f2 o f1)%functor
n1: f0 <~=~> (f1 o f3)%functor
n2: f <~=~> (f2 o f0)%functor
IsIsomorphism
  (n2^-1
   o (f2 oL n1^-1
      o (associator_1 f2 f1 f3 o (n0 oR f3 o n))))%natural_transformation
    Proof.H: Funext
C: PreCategory
F: Pseudofunctor C
w, x, y, z: C
f: Functor (F w) (F z)
f0: Functor (F w) (F y)
f1: Functor (F x) (F y)
f2: Functor (F y) (F z)
f3: Functor (F w) (F x)
f4: Functor (F x) (F z)
f5: Functor (F w) (F z)
n: f5 <~=~> (f4 o f3)%functor
n0: f4 <~=~> (f2 o f1)%functor
n1: f0 <~=~> (f1 o f3)%functor
n2: f <~=~> (f2 o f0)%functor
IsIsomorphism
  (n2^-1
   o (f2 oL n1^-1
      o (associator_1 f2 f1 f3 o (n0 oR f3 o n))))%natural_transformation
      eapply isisomorphism_compose;
      [ eapply isisomorphism_inverse
      | eapply isisomorphism_compose;
        [ eapply iso_whisker_l; eapply isisomorphism_inverse
        | eapply isisomorphism_compose;
          [ typeclasses eauto
          | eapply isisomorphism_compose;
            [ eapply iso_whisker_r; typeclasses eauto
            | typeclasses eauto ] ] ] ].
    Defined.

    Definition p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper
      := Eval hnf in p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper'.

    Local Arguments p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper / .
    Let inv := Eval simpl in @morphism_inverse _ _ _ _ p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper.

    Definition p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper__to_inverse
          X
          (H' : X = @Build_Isomorphic (_ -> _) _ _ _ p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper)
    : @morphism_inverse _ _ _ _ X = inv
      := ap (fun i => @morphism_inverse _ _ _ _ (@isisomorphism_isomorphic _ _ _ i)) H'.
  End helper.

  Lemma p_composition_of_coherent_iso_for_rewrite w x y z
        (f : morphism C w x) (g : morphism C x y) (h : morphism C y z)
  : (Category.Morphisms.idtoiso (_ -> _) (ap (@p_morphism_of _ _ F w z) (Category.Core.associativity C w x y z f g h)))
    = @Build_Isomorphic
        (_ -> _) _ _
        ((((p_composition_of F w y z h (g o f))^-1)
            o ((p_morphism_of F h oL (p_composition_of F w x y g f)^-1)
                 o ((associator_1 (p_morphism_of F h) (p_morphism_of F g) (p_morphism_of F f))
                      o ((p_composition_of F x y z h g oR p_morphism_of F f)
                           o p_composition_of F w x z (h o g) f)))))%natural_transformation
        p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper.H: Funext
C: PreCategory
F: Pseudofunctor C
w, x, y, z: C
f: morphism C w x
g: morphism C x y
h: morphism C y z
Category.Morphisms.idtoiso (F w -> F z)
  (ap (p_morphism_of F)
     (Core.associativity C w x y z f g h)) =
{|
  morphism_isomorphic :=
    ((p_composition_of F w y z h (g o f))^-1
     o (p_morphism_of F h
        oL (p_composition_of F w x y g f)^-1
        o (associator_1 (p_morphism_of F h)
             (p_morphism_of F g) (p_morphism_of F f)
           o (p_composition_of F x y z h g
              oR p_morphism_of F f
              o p_composition_of F w x z (h o g) f))))%natural_transformation;
  isisomorphism_isomorphic :=
    p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper
|}
  Proof.H: Funext
C: PreCategory
F: Pseudofunctor C
w, x, y, z: C
f: morphism C w x
g: morphism C x y
h: morphism C y z
Category.Morphisms.idtoiso (F w -> F z)
  (ap (p_morphism_of F)
     (Core.associativity C w x y z f g h)) =
{|
  morphism_isomorphic :=
    ((p_composition_of F w y z h (g o f))^-1
     o (p_morphism_of F h
        oL (p_composition_of F w x y g f)^-1
        o (associator_1 (p_morphism_of F h)
             (p_morphism_of F g) (p_morphism_of F f)
           o (p_composition_of F x y z h g
              oR p_morphism_of F f
              o p_composition_of F w x z (h o g) f))))%natural_transformation;
  isisomorphism_isomorphic :=
    p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper
|}
    apply path_isomorphic; simpl.H: Funext
C: PreCategory
F: Pseudofunctor C
w, x, y, z: C
f: morphism C w x
g: morphism C x y
h: morphism C y z
Category.Morphisms.idtoiso (F w -> F z)
  (ap (p_morphism_of F)
     (Core.associativity C w x y z f g h)) =
(p_composition_of F w y z h (g o f))^-1
o (p_morphism_of F h
   oL (p_composition_of F w x y g f)^-1
   o (associator_1 (p_morphism_of F h)
        (p_morphism_of F g) (p_morphism_of F f)
      o (p_composition_of F x y z h g
         oR p_morphism_of F f
         o p_composition_of F w x z (h o g) f)))
    simpl rewrite (@p_composition_of_coherent _ C F w x y z f g h).H: Funext
C: PreCategory
F: Pseudofunctor C
w, x, y, z: C
f: morphism C w x
g: morphism C x y
h: morphism C y z
Category.Morphisms.idtoiso (F w -> F z)
  (ap (p_morphism_of F)
     (Core.associativity C w x y z f g h)) =
(p_composition_of F w y z h (g o f))^-1
o (p_morphism_of F h
   oL (p_composition_of F w x y g f)^-1
   o (p_morphism_of F h
      oL p_composition_of F w x y g f
      o (p_composition_of F w y z h (g o f)
         o Category.Morphisms.idtoiso (F w -> F z)
             (ap (p_morphism_of F)
                (Core.associativity C w x y z f g h)))))
    exact p_composition_of_coherent_for_rewrite_helper.
  Qed.

  Lemma p_left_identity_of_coherent_iso_for_rewrite x y (f : morphism C x y)
  : (Category.Morphisms.idtoiso (_ -> _) (ap (@p_morphism_of _ _ F x y) (Category.Core.left_identity C x y f)))
    = @Build_Isomorphic
        (_ -> _) _ _
        ((left_identity_natural_transformation_1 (p_morphism_of F f))
           o ((p_identity_of F y oR p_morphism_of F f)
                o p_composition_of F x y y 1 f))%natural_transformation
        _.H: Funext
C: PreCategory
F: Pseudofunctor C
x, y: C
f: morphism C x y
Category.Morphisms.idtoiso (F x -> F y)
  (ap (p_morphism_of F) (Core.left_identity C x y f)) =
{|
  morphism_isomorphic :=
    (left_identity_natural_transformation_1
       (p_morphism_of F f)
     o (p_identity_of F y oR p_morphism_of F f
        o p_composition_of F x y y 1 f))%natural_transformation;
  isisomorphism_isomorphic :=
    isisomorphism_compose
      (left_identity_natural_transformation_1
         (p_morphism_of F f))
      (p_identity_of F y oR p_morphism_of F f
       o p_composition_of F x y y 1 f)
|}
  Proof.H: Funext
C: PreCategory
F: Pseudofunctor C
x, y: C
f: morphism C x y
Category.Morphisms.idtoiso (F x -> F y)
  (ap (p_morphism_of F) (Core.left_identity C x y f)) =
{|
  morphism_isomorphic :=
    (left_identity_natural_transformation_1
       (p_morphism_of F f)
     o (p_identity_of F y oR p_morphism_of F f
        o p_composition_of F x y y 1 f))%natural_transformation;
  isisomorphism_isomorphic :=
    isisomorphism_compose
      (left_identity_natural_transformation_1
         (p_morphism_of F f))
      (p_identity_of F y oR p_morphism_of F f
       o p_composition_of F x y y 1 f)
|}
    apply path_isomorphic; simpl.H: Funext
C: PreCategory
F: Pseudofunctor C
x, y: C
f: morphism C x y
Category.Morphisms.idtoiso (F x -> F y)
  (ap (p_morphism_of F) (Core.left_identity C x y f)) =
left_identity_natural_transformation_1
  (p_morphism_of F f)
o (p_identity_of F y oR p_morphism_of F f
   o p_composition_of F x y y 1 f)
    simpl rewrite (@p_left_identity_of_coherent _ C F x y f).H: Funext
C: PreCategory
F: Pseudofunctor C
x, y: C
f: morphism C x y
Category.Morphisms.idtoiso (F x -> F y)
  (ap (p_morphism_of F) (Core.left_identity C x y f)) =
left_identity_natural_transformation_1
  (p_morphism_of F f)
o (left_identity_natural_transformation_2
     (p_morphism_of F f)
   o Category.Morphisms.idtoiso (F x -> F y)
       (ap (p_morphism_of F)
          (Core.left_identity C x y f)))
    path_natural_transformation.H: Funext
C: PreCategory
F: Pseudofunctor C
x, y: C
f: morphism C x y
x0: F x
Category.Morphisms.idtoiso (F x -> F y)
  (ap (p_morphism_of F) (Core.left_identity C x y f))
  x0 =
(1
 o (1
    o Category.Morphisms.idtoiso (F x -> F y)
        (ap (p_morphism_of F)
           (Core.left_identity C x y f)) x0))%morphism
    symmetry.H: Funext
C: PreCategory
F: Pseudofunctor C
x, y: C
f: morphism C x y
x0: F x
(1
 o (1
    o Category.Morphisms.idtoiso (F x -> F y)
        (ap (p_morphism_of F)
           (Core.left_identity C x y f)) x0))%morphism =
Category.Morphisms.idtoiso (F x -> F y)
  (ap (p_morphism_of F) (Core.left_identity C x y f))
  x0
    etransitivity; apply Category.Core.left_identity.
  Qed.

  Lemma p_right_identity_of_coherent_iso_for_rewrite x y (f : morphism C x y)
  : (Category.Morphisms.idtoiso (_ -> _) (ap (@p_morphism_of _ _ F x y) (Category.Core.right_identity C x y f)))
    = @Build_Isomorphic
        (_ -> _) _ _
        ((right_identity_natural_transformation_1 (p_morphism_of F f))
           o ((p_morphism_of F f oL p_identity_of F x)
                o p_composition_of F x x y f 1))%natural_transformation
        _.H: Funext
C: PreCategory
F: Pseudofunctor C
x, y: C
f: morphism C x y
Category.Morphisms.idtoiso (F x -> F y)
  (ap (p_morphism_of F) (Core.right_identity C x y f)) =
{|
  morphism_isomorphic :=
    (right_identity_natural_transformation_1
       (p_morphism_of F f)
     o (p_morphism_of F f oL p_identity_of F x
        o p_composition_of F x x y f 1))%natural_transformation;
  isisomorphism_isomorphic :=
    isisomorphism_compose
      (right_identity_natural_transformation_1
         (p_morphism_of F f))
      (p_morphism_of F f oL p_identity_of F x
       o p_composition_of F x x y f 1)
|}
  Proof.H: Funext
C: PreCategory
F: Pseudofunctor C
x, y: C
f: morphism C x y
Category.Morphisms.idtoiso (F x -> F y)
  (ap (p_morphism_of F) (Core.right_identity C x y f)) =
{|
  morphism_isomorphic :=
    (right_identity_natural_transformation_1
       (p_morphism_of F f)
     o (p_morphism_of F f oL p_identity_of F x
        o p_composition_of F x x y f 1))%natural_transformation;
  isisomorphism_isomorphic :=
    isisomorphism_compose
      (right_identity_natural_transformation_1
         (p_morphism_of F f))
      (p_morphism_of F f oL p_identity_of F x
       o p_composition_of F x x y f 1)
|}
    apply path_isomorphic; simpl.H: Funext
C: PreCategory
F: Pseudofunctor C
x, y: C
f: morphism C x y
Category.Morphisms.idtoiso (F x -> F y)
  (ap (p_morphism_of F) (Core.right_identity C x y f)) =
right_identity_natural_transformation_1
  (p_morphism_of F f)
o (p_morphism_of F f oL p_identity_of F x
   o p_composition_of F x x y f 1)
    simpl rewrite (@p_right_identity_of_coherent _ C F x y f).H: Funext
C: PreCategory
F: Pseudofunctor C
x, y: C
f: morphism C x y
Category.Morphisms.idtoiso (F x -> F y)
  (ap (p_morphism_of F) (Core.right_identity C x y f)) =
right_identity_natural_transformation_1
  (p_morphism_of F f)
o (right_identity_natural_transformation_2
     (p_morphism_of F f)
   o Category.Morphisms.idtoiso (F x -> F y)
       (ap (p_morphism_of F)
          (Core.right_identity C x y f)))
    path_natural_transformation.H: Funext
C: PreCategory
F: Pseudofunctor C
x, y: C
f: morphism C x y
x0: F x
Category.Morphisms.idtoiso (F x -> F y)
  (ap (p_morphism_of F) (Core.right_identity C x y f))
  x0 =
(1
 o (1
    o Category.Morphisms.idtoiso (F x -> F y)
        (ap (p_morphism_of F)
           (Core.right_identity C x y f)) x0))%morphism
    symmetry.H: Funext
C: PreCategory
F: Pseudofunctor C
x, y: C
f: morphism C x y
x0: F x
(1
 o (1
    o Category.Morphisms.idtoiso (F x -> F y)
        (ap (p_morphism_of F)
           (Core.right_identity C x y f)) x0))%morphism =
Category.Morphisms.idtoiso (F x -> F y)
  (ap (p_morphism_of F) (Core.right_identity C x y f))
  x0
    etransitivity; apply Category.Core.left_identity.
  Qed.

  Local Notation typeof x := ((fun T (_ : T) => T) _ x) (only parsing).

  Let p_composition_of_coherent_for_rewrite_type w x y z f g h
    := Eval simpl in typeof (ap (@morphism_isomorphic _ _ _)
                                (@p_composition_of_coherent_iso_for_rewrite w x y z f g h)).
  Definition p_composition_of_coherent_for_rewrite w x y z f g h
  : p_composition_of_coherent_for_rewrite_type w x y z f g h
    := ap (@morphism_isomorphic _ _ _)
          (@p_composition_of_coherent_iso_for_rewrite w x y z f g h).

  Let p_composition_of_coherent_inverse_for_rewrite_type w x y z f g h
    := Eval simpl in typeof (ap (fun i => @morphism_inverse _ _ _ _ (@isisomorphism_isomorphic _ _ _ i))
                                (@p_composition_of_coherent_iso_for_rewrite w x y z f g h)).
  Definition p_composition_of_coherent_inverse_for_rewrite w x y z f g h
  : p_composition_of_coherent_inverse_for_rewrite_type w x y z f g h
    := p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper__to_inverse
         (p_composition_of_coherent_iso_for_rewrite w x y z f g h).

  Let p_left_identity_of_coherent_for_rewrite_type x y f
    := Eval simpl in typeof (ap (@morphism_isomorphic _ _ _)
                                (@p_left_identity_of_coherent_iso_for_rewrite x y f)).
  Definition p_left_identity_of_coherent_for_rewrite x y f
  : p_left_identity_of_coherent_for_rewrite_type x y f
    := ap (@morphism_isomorphic _ _ _)
          (@p_left_identity_of_coherent_iso_for_rewrite x y f).

  Let p_left_identity_of_coherent_inverse_for_rewrite_type x y f
    := Eval simpl in typeof (ap (fun i => @morphism_inverse _ _ _ _ (@isisomorphism_isomorphic _ _ _ i))
                                (@p_left_identity_of_coherent_iso_for_rewrite x y f)).
  Definition p_left_identity_of_coherent_inverse_for_rewrite x y f
  : p_left_identity_of_coherent_inverse_for_rewrite_type x y f
    := ap (fun i => @morphism_inverse _ _ _ _ (@isisomorphism_isomorphic _ _ _ i))
          (@p_left_identity_of_coherent_iso_for_rewrite x y f).

  Let p_right_identity_of_coherent_for_rewrite_type x y f
    := Eval simpl in typeof (ap (@morphism_isomorphic _ _ _)
                                (@p_right_identity_of_coherent_iso_for_rewrite x y f)).
  Definition p_right_identity_of_coherent_for_rewrite x y f
  : p_right_identity_of_coherent_for_rewrite_type x y f
    := Eval simpl in ap (@morphism_isomorphic _ _ _)
                        (@p_right_identity_of_coherent_iso_for_rewrite x y f).

  Let p_right_identity_of_coherent_inverse_for_rewrite_type x y f
    := Eval simpl in typeof (ap (fun i => @morphism_inverse _ _ _ _ (@isisomorphism_isomorphic _ _ _ i))
                                (@p_right_identity_of_coherent_iso_for_rewrite x y f)).
  Definition p_right_identity_of_coherent_inverse_for_rewrite x y f
  : p_right_identity_of_coherent_inverse_for_rewrite_type x y f
    := ap (fun i => @morphism_inverse _ _ _ _ (@isisomorphism_isomorphic _ _ _ i))
          (@p_right_identity_of_coherent_iso_for_rewrite x y f).
End lemmas.