NatTrans.v

Require Import Basics.Overture Basics.Tactics.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.Core.
Require Import WildCat.Equiv.
Require Import WildCat.Square.
Require Import WildCat.Opposite.

(** ** Natural transformations *)

Definition Transformation {A : Type} {B : A -> Type} `{forall x, IsGraph (B x)}
  (F G : forall (x : A), B x)
  := forall (a : A), F a $-> G a.

(** This lets us apply transformations to things. Identity Coercion tells coq that this coercion is in fact definitionally the identity map so it doesn't need to insert it, but merely rewrite definitionally when typechecking. *)
Identity Coercion fun_trans : Transformation >-> Funclass.

Notation "F $=> G" := (Transformation F G).

(** A 1-natural transformation is natural up to a 2-cell, so its codomain must be a 1-category. *)
Class Is1Natural {A B : Type} `{IsGraph A} `{Is1Cat B}
      (F : A -> B) `{!Is0Functor F} (G : A -> B) `{!Is0Functor G}
      (alpha : F $=> G) :=
  isnat : forall a a' (f : a $-> a'),
     (alpha a') $o (fmap F f) $== (fmap G f) $o (alpha a).

Arguments Is1Natural {A B} {isgraph_A}
  {isgraph_B} {is2graph_B} {is01cat_B} {is1cat_B}
  F {is0functor_F} G {is0functor_G} alpha : rename.
Arguments isnat {_ _ _ _ _ _ _ _ _ _ _} alpha {alnat _ _} f : rename.

Record NatTrans {A B : Type} `{IsGraph A} `{Is1Cat B} {F G : A -> B}
  {ff : Is0Functor F} {fg : Is0Functor G} :=
{
  trans_nattrans : F $=> G ;
  is1natural_nattrans : Is1Natural F G trans_nattrans ;
}.

Arguments NatTrans {A B} {isgraph_A}
  {isgraph_B} {is2graph_B} {is01cat_B} {is1cat_B}
  F G {is0functor_F} {is0functor_G} : rename.
Arguments Build_NatTrans {A B} {isgraph_A}
  {isgraph_B} {is2graph_B} {is01cat_B} {is1cat_B}
  F G {is0functor_F} {is0functor_G} alpha isnat_alpha: rename.

Global Existing Instance is1natural_nattrans.
Coercion trans_nattrans : NatTrans >-> Transformation.

Definition issig_NatTrans {A B : Type} `{IsGraph A} `{Is1Cat B} (F G : A -> B)
  {ff : Is0Functor F} {fg : Is0Functor G}
  : _ <~> NatTrans F G := ltac:(issig).

(** The transposed natural square *)
Definition isnat_tr {A B : Type} `{IsGraph A} `{Is1Cat B}
      {F : A -> B} `{!Is0Functor F} {G : A -> B} `{!Is0Functor G}
      (alpha : F $=> G) `{!Is1Natural F G alpha}
      {a a' : A} (f : a $-> a')
  : (fmap G f) $o (alpha a) $== (alpha a') $o (fmap F f)
  := (isnat alpha f)^$.

Definition id_transformation {A B : Type} `{Is01Cat B} (F : A -> B)
  : F $=> F
  := fun a => Id (F a).

Global Instance is1natural_id {A B : Type} `{IsGraph A} `{Is1Cat B}
       (F : A -> B) `{!Is0Functor F}
  : Is1Natural F F (id_transformation F).A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
Is0Functor0: Is0Functor F
Is1Natural F F (id_transformation F)
Proof.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
Is0Functor0: Is0Functor F
Is1Natural F F (id_transformation F)
  intros a b f; cbn.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
Is0Functor0: Is0Functor F
a, b: A
f: a $-> b
id_transformation F b $o fmap F f $==
fmap F f $o id_transformation F a
  refine (cat_idl _ $@ (cat_idr _)^$).
Defined.

Definition nattrans_id {A B : Type} (F : A -> B)
  `{IsGraph A, Is1Cat B, !Is0Functor F}
  : NatTrans F F.A, B: Type
F: A -> B
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
NatTrans F F
Proof.A, B: Type
F: A -> B
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
NatTrans F F
  nrapply Build_NatTrans.A, B: Type
F: A -> B
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is1Natural F F ?Goal
  rapply is1natural_id.
Defined.

Definition trans_comp {A B : Type} `{Is01Cat B}
           {F G K : A -> B} (gamma : G $=> K) (alpha : F $=> G)
  : F $=> K
  := fun a => gamma a $o alpha a.

Definition trans_prewhisker {A B : Type} {C : B -> Type} {F G : forall x, C x}
  `{Is01Cat B} `{!forall x, IsGraph (C x)}
  `{!forall x, Is01Cat (C x)} (gamma : F $=> G) (K : A -> B) 
  : F o K $=> G o K
  := gamma o K.

Definition trans_postwhisker {A B C : Type} {F G : A -> B}
  (K : B -> C) `{Is01Cat B, Is01Cat C, !Is0Functor K} (gamma : F $=> G)
  : K o F $=> K o G
  := fun a => fmap K (gamma a).

Global Instance is1natural_comp {A B : Type} `{IsGraph A} `{Is1Cat B}
       {F G K : A -> B} `{!Is0Functor F} `{!Is0Functor G} `{!Is0Functor K}
       (gamma : G $=> K) `{!Is1Natural G K gamma}
       (alpha : F $=> G) `{!Is1Natural F G alpha}
  : Is1Natural F K (trans_comp gamma alpha).A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F, G, K: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
gamma: G $=> K
Is1Natural0: Is1Natural G K gamma
alpha: F $=> G
Is1Natural1: Is1Natural F G alpha
Is1Natural F K (trans_comp gamma alpha)
Proof.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F, G, K: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
gamma: G $=> K
Is1Natural0: Is1Natural G K gamma
alpha: F $=> G
Is1Natural1: Is1Natural F G alpha
Is1Natural F K (trans_comp gamma alpha)
  intros a b f; unfold trans_comp; cbn.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F, G, K: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
gamma: G $=> K
Is1Natural0: Is1Natural G K gamma
alpha: F $=> G
Is1Natural1: Is1Natural F G alpha
a, b: A
f: a $-> b
gamma b $o alpha b $o fmap F f $==
fmap K f $o (gamma a $o alpha a)
  refine (cat_assoc _ _ _ $@ (_ $@L isnat alpha f) $@ _).A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F, G, K: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
gamma: G $=> K
Is1Natural0: Is1Natural G K gamma
alpha: F $=> G
Is1Natural1: Is1Natural F G alpha
a, b: A
f: a $-> b
gamma b $o (fmap G f $o alpha a) $==
fmap K f $o (gamma a $o alpha a)
  refine (cat_assoc_opp _ _ _ $@ (isnat gamma f $@R _) $@ _).A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F, G, K: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
gamma: G $=> K
Is1Natural0: Is1Natural G K gamma
alpha: F $=> G
Is1Natural1: Is1Natural F G alpha
a, b: A
f: a $-> b
fmap K f $o gamma a $o alpha a $==
fmap K f $o (gamma a $o alpha a)
  apply cat_assoc.
Defined.

Global Instance is1natural_prewhisker {A B C : Type} {F G : B -> C} (K : A -> B)
  `{IsGraph A, Is01Cat B, Is1Cat C, !Is0Functor F, !Is0Functor G, !Is0Functor K}
  (gamma : F $=> G) `{L : !Is1Natural F G gamma}
  : Is1Natural (F o K) (G o K) (trans_prewhisker gamma K).A, B, C: Type
F, G: B -> C
K: A -> B
H: IsGraph A
H0: IsGraph B
H1: Is01Cat B
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H2: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
gamma: F $=> G
L: Is1Natural F G gamma
Is1Natural (F o K) (G o K) (trans_prewhisker gamma K)
Proof.A, B, C: Type
F, G: B -> C
K: A -> B
H: IsGraph A
H0: IsGraph B
H1: Is01Cat B
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H2: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
gamma: F $=> G
L: Is1Natural F G gamma
Is1Natural (F o K) (G o K) (trans_prewhisker gamma K)
  intros x y f; unfold trans_prewhisker; cbn.A, B, C: Type
F, G: B -> C
K: A -> B
H: IsGraph A
H0: IsGraph B
H1: Is01Cat B
IsGraph0: IsGraph C
Is2Graph0: Is2Graph C
Is01Cat0: Is01Cat C
H2: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
gamma: F $=> G
L: Is1Natural F G gamma
x, y: A
f: x $-> y
gamma (K y) $o fmap F (fmap K f) $==
fmap G (fmap K f) $o gamma (K x)
  exact (L _ _ _).
Defined.

Global Instance is1natural_postwhisker {A B C : Type} {F G : A -> B} (K : B -> C)
 `{IsGraph A, Is1Cat B, Is1Cat C, !Is0Functor F, !Is0Functor G, !Is0Functor K, !Is1Functor K}
  (gamma : F $=> G) `{L : !Is1Natural F G gamma}
  : Is1Natural (K o F) (K o G) (trans_postwhisker K gamma).A, B, C: Type
F, G: A -> B
K: B -> C
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
gamma: F $=> G
L: Is1Natural F G gamma
Is1Natural (K o F) (K o G) (trans_postwhisker K gamma)
Proof.A, B, C: Type
F, G: A -> B
K: B -> C
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
gamma: F $=> G
L: Is1Natural F G gamma
Is1Natural (K o F) (K o G) (trans_postwhisker K gamma)
  intros x y f; unfold trans_postwhisker; cbn.A, B, C: Type
F, G: A -> B
K: B -> C
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
gamma: F $=> G
L: Is1Natural F G gamma
x, y: A
f: x $-> y
fmap K (gamma y) $o fmap K (fmap F f) $==
fmap K (fmap G f) $o fmap K (gamma x)
  refine (_^$ $@ _ $@ _).A, B, C: Type
F, G: A -> B
K: B -> C
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
gamma: F $=> G
L: Is1Natural F G gamma
x, y: A
f: x $-> y
?Goal0 $-> fmap K (gamma y) $o fmap K (fmap F f)
A, B, C: Type
F, G: A -> B
K: B -> C
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
gamma: F $=> G
L: Is1Natural F G gamma
x, y: A
f: x $-> y
?Goal0 $== ?Goal
A, B, C: Type
F, G: A -> B
K: B -> C
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
gamma: F $=> G
L: Is1Natural F G gamma
x, y: A
f: x $-> y
?Goal $== fmap K (fmap G f) $o fmap K (gamma x)
  1,3: rapply fmap_comp.A, B, C: Type
F, G: A -> B
K: B -> C
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
gamma: F $=> G
L: Is1Natural F G gamma
x, y: A
f: x $-> y
fmap K (gamma y $o fmap F f) $==
fmap K (fmap G f $o gamma x)
  rapply fmap2.A, B, C: Type
F, G: A -> B
K: B -> C
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
gamma: F $=> G
L: Is1Natural F G gamma
x, y: A
f: x $-> y
gamma y $o fmap F f $== fmap G f $o gamma x
  exact (L _ _ _).
Defined.

Definition nattrans_comp {A B : Type} {F G K : A -> B}
  `{IsGraph A, Is1Cat B, !Is0Functor F, !Is0Functor G, !Is0Functor K}
  : NatTrans G K -> NatTrans F G -> NatTrans F K.A, B: Type
F, G, K: A -> B
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
NatTrans G K -> NatTrans F G -> NatTrans F K
Proof.A, B: Type
F, G, K: A -> B
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
NatTrans G K -> NatTrans F G -> NatTrans F K
  intros alpha beta.A, B: Type
F, G, K: A -> B
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
alpha: NatTrans G K
beta: NatTrans F G
NatTrans F K
  nrapply Build_NatTrans.A, B: Type
F, G, K: A -> B
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
alpha: NatTrans G K
beta: NatTrans F G
Is1Natural F K ?Goal
  rapply (is1natural_comp alpha beta).
Defined.

Definition nattrans_prewhisker {A B C : Type} {F G : B -> C}
  `{IsGraph A, Is1Cat B, Is1Cat C, !Is0Functor F, !Is0Functor G}
  (alpha : NatTrans F G) (K : A -> B) `{!Is0Functor K} 
  : NatTrans (F o K) (G o K).A, B, C: Type
F, G: B -> C
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: NatTrans F G
K: A -> B
Is0Functor2: Is0Functor K
NatTrans (F o K) (G o K)
Proof.A, B, C: Type
F, G: B -> C
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: NatTrans F G
K: A -> B
Is0Functor2: Is0Functor K
NatTrans (F o K) (G o K)
  nrapply Build_NatTrans.A, B, C: Type
F, G: B -> C
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: NatTrans F G
K: A -> B
Is0Functor2: Is0Functor K
Is1Natural (fun x : A => F (K x))
  (fun x : A => G (K x)) ?Goal
  rapply (is1natural_prewhisker K alpha).
Defined.

Definition nattrans_postwhisker {A B C : Type} {F G : A -> B} (K : B -> C)
  `{IsGraph A, Is1Cat B, Is1Cat C, !Is0Functor F, !Is0Functor G,
    !Is0Functor K, !Is1Functor K} 
  : NatTrans F G -> NatTrans (K o F) (K o G).A, B, C: Type
F, G: A -> B
K: B -> C
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
NatTrans F G -> NatTrans (K o F) (K o G)
Proof.A, B, C: Type
F, G: A -> B
K: B -> C
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
NatTrans F G -> NatTrans (K o F) (K o G)
  intros alpha.A, B, C: Type
F, G: A -> B
K: B -> C
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
alpha: NatTrans F G
NatTrans (K o F) (K o G)
  nrapply Build_NatTrans.A, B, C: Type
F, G: A -> B
K: B -> C
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H1: Is1Cat C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
alpha: NatTrans F G
Is1Natural (fun x : A => K (F x))
  (fun x : A => K (G x)) ?Goal
  rapply (is1natural_postwhisker K alpha).
Defined.

(** Modifying a transformation to something pointwise equal preserves naturality. *)
Definition is1natural_homotopic {A B : Type} `{Is01Cat A} `{Is1Cat B}
      {F : A -> B} `{!Is0Functor F} {G : A -> B} `{!Is0Functor G}
      {alpha : F $=> G} (gamma : F $=> G) `{!Is1Natural F G gamma}
      (p : forall a, alpha a $== gamma a)
  : Is1Natural F G alpha.A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
F: A -> B
Is0Functor0: Is0Functor F
G: A -> B
Is0Functor1: Is0Functor G
alpha, gamma: F $=> G
Is1Natural0: Is1Natural F G gamma
p: forall a : A, alpha a $== gamma a
Is1Natural F G alpha
Proof.A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
F: A -> B
Is0Functor0: Is0Functor F
G: A -> B
Is0Functor1: Is0Functor G
alpha, gamma: F $=> G
Is1Natural0: Is1Natural F G gamma
p: forall a : A, alpha a $== gamma a
Is1Natural F G alpha
  intros a b f.A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
F: A -> B
Is0Functor0: Is0Functor F
G: A -> B
Is0Functor1: Is0Functor G
alpha, gamma: F $=> G
Is1Natural0: Is1Natural F G gamma
p: forall a : A, alpha a $== gamma a
a, b: A
f: a $-> b
alpha b $o fmap F f $== fmap G f $o alpha a
  exact ((p b $@R _) $@ isnat gamma f $@ (_ $@L (p a)^$)).
Defined.

(** Opposite natural transformations *)

Definition transformation_op {A} {B} `{Is01Cat B}
           (F : A -> B) (G : A -> B) (alpha : F $=> G)
  : @Transformation A^op (fun _ => B^op) _
                     (G : A^op -> B^op) (F : A^op -> B^op).A, B: Type
H: IsGraph B
H0: Is01Cat B
F, G: A -> B
alpha: F $=> G
(G : A^op -> B^op) $=> (F : A^op -> B^op)
Proof.A, B: Type
H: IsGraph B
H0: Is01Cat B
F, G: A -> B
alpha: F $=> G
(G : A^op -> B^op) $=> (F : A^op -> B^op)
  unfold op in *.A, B: Type
H: IsGraph B
H0: Is01Cat B
F, G: A -> B
alpha: F $=> G
G $=> F
  cbn in *.A, B: Type
H: IsGraph B
H0: Is01Cat B
F, G: A -> B
alpha: F $=> G
G $=> F
  intro a.A, B: Type
H: IsGraph B
H0: Is01Cat B
F, G: A -> B
alpha: F $=> G
a: A
G a $-> F a
  apply (alpha a).
Defined.

Global Instance is1nat_op A B `{Is01Cat A} `{Is1Cat B}
       (F : A -> B) `{!Is0Functor F}
       (G : A -> B) `{!Is0Functor G}
       (alpha : F $=> G) `{!Is1Natural F G alpha}
  : Is1Natural (G : A^op -> B^op) (F : A^op -> B^op) (transformation_op F G alpha).A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
F: A -> B
Is0Functor0: Is0Functor F
G: A -> B
Is0Functor1: Is0Functor G
alpha: F $=> G
Is1Natural0: Is1Natural F G alpha
Is1Natural (G : A^op -> B^op) (F : A^op -> B^op)
  (transformation_op F G alpha)
Proof.A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
F: A -> B
Is0Functor0: Is0Functor F
G: A -> B
Is0Functor1: Is0Functor G
alpha: F $=> G
Is1Natural0: Is1Natural F G alpha
Is1Natural (G : A^op -> B^op) (F : A^op -> B^op)
  (transformation_op F G alpha)
  unfold op.A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
F: A -> B
Is0Functor0: Is0Functor F
G: A -> B
Is0Functor1: Is0Functor G
alpha: F $=> G
Is1Natural0: Is1Natural F G alpha
Is1Natural G F (transformation_op F G alpha)
  unfold transformation_op.A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
F: A -> B
Is0Functor0: Is0Functor F
G: A -> B
Is0Functor1: Is0Functor G
alpha: F $=> G
Is1Natural0: Is1Natural F G alpha
Is1Natural G F (fun a : A => alpha a)
  intros a b f.A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
F: A -> B
Is0Functor0: Is0Functor F
G: A -> B
Is0Functor1: Is0Functor G
alpha: F $=> G
Is1Natural0: Is1Natural F G alpha
a, b: A
f: a $-> b
alpha b $o fmap (G : A^op -> B^op) f $==
fmap (F : A^op -> B^op) f $o alpha a
  srapply isnat_tr.
Defined.

(** Natural equivalences *)

Record NatEquiv {A B : Type} `{IsGraph A} `{HasEquivs B}
  {F G : A -> B} `{!Is0Functor F, !Is0Functor G} :=
{
  cat_equiv_natequiv : forall a, F a $<~> G a ;
  is1natural_natequiv : Is1Natural F G (fun a => cat_equiv_natequiv a) ;
}.

Arguments NatEquiv {A B} {isgraph_A}
  {isgraph_B} {is2graph_B} {is01cat_B} {is1cat_B} {hasequivs_B}
  F G {is0functor_F} {is0functor_G} : rename.
Arguments Build_NatEquiv {A B} {isgraph_A}
  {isgraph_B} {is2graph_B} {is01cat_B} {is1cat_B} {hasequivs_B}
  F G {is0functor_F} {is0functor_G} e isnat_e: rename.

Definition issig_NatEquiv {A B : Type} `{IsGraph A} `{HasEquivs B}
  (F G : A -> B) `{!Is0Functor F, !Is0Functor G}
  : _ <~> NatEquiv F G := ltac:(issig).

Global Existing Instance is1natural_natequiv.
Coercion cat_equiv_natequiv : NatEquiv >-> Funclass.

Lemma nattrans_natequiv {A B : Type} `{IsGraph A} `{HasEquivs B}
  {F G : A -> B} `{!Is0Functor F, !Is0Functor G}
  : NatEquiv F G -> NatTrans F G.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
NatEquiv F G -> NatTrans F G
Proof.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
NatEquiv F G -> NatTrans F G
  intros alpha.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: NatEquiv F G
NatTrans F G
  nrapply Build_NatTrans.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: NatEquiv F G
Is1Natural F G ?Goal
  rapply (is1natural_natequiv alpha).
Defined.

(** Throws a warning, but can probably be ignored. *)
Global Set Warnings "-ambiguous-paths".
Coercion nattrans_natequiv : NatEquiv >-> NatTrans.

(** The above coercion doesn't trigger when it should, so we add the following. *)
Definition isnat_natequiv {A B : Type} `{IsGraph A} `{HasEquivs B}
  {F G : A -> B} `{!Is0Functor F, !Is0Functor G} (alpha : NatEquiv F G)
  {a a' : A} (f : a $-> a')
  := isnat (nattrans_natequiv alpha) f.

Definition Build_NatEquiv' {A B : Type} `{IsGraph A} `{HasEquivs B}
  {F G : A -> B} `{!Is0Functor F, !Is0Functor G}
  (alpha : NatTrans F G) `{forall a, CatIsEquiv (alpha a)}
  : NatEquiv F G.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: NatTrans F G
H2: forall a : A, CatIsEquiv (alpha a)
NatEquiv F G
Proof.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: NatTrans F G
H2: forall a : A, CatIsEquiv (alpha a)
NatEquiv F G
  snrapply Build_NatEquiv.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: NatTrans F G
H2: forall a : A, CatIsEquiv (alpha a)
forall a : A, F a $<~> G a
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: NatTrans F G
H2: forall a : A, CatIsEquiv (alpha a)
Is1Natural F G (fun a : A => ?e a)
  -A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: NatTrans F G
H2: forall a : A, CatIsEquiv (alpha a)
forall a : A, F a $<~> G a intro a.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: NatTrans F G
H2: forall a : A, CatIsEquiv (alpha a)
a: A
F a $<~> G a
    refine (Build_CatEquiv (alpha a)).
  -A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: NatTrans F G
H2: forall a : A, CatIsEquiv (alpha a)
Is1Natural F G
  (fun a : A =>
   (fun a0 : A => Build_CatEquiv (alpha a0)) a) intros a a' f.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: NatTrans F G
H2: forall a : A, CatIsEquiv (alpha a)
a, a': A
f: a $-> a'
Build_CatEquiv (alpha a') $o fmap F f $==
fmap G f $o Build_CatEquiv (alpha a)
    refine (cate_buildequiv_fun _ $@R _ $@ _ $@ (_ $@L cate_buildequiv_fun _)^$).A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: NatTrans F G
H2: forall a : A, CatIsEquiv (alpha a)
a, a': A
f: a $-> a'
alpha a' $o fmap F f $== fmap G f $o alpha a
    apply (isnat alpha).
Defined.

Definition natequiv_compose {A B} {F G H : A -> B} `{IsGraph A} `{HasEquivs B}
  `{!Is0Functor F, !Is0Functor G, !Is0Functor H}
  (alpha : NatEquiv G H) (beta : NatEquiv F G)
  : NatEquiv F H
  := Build_NatEquiv' (nattrans_comp alpha beta).

Definition natequiv_prewhisker {A B C} {H K : B -> C}
  `{IsGraph A, HasEquivs B, HasEquivs C, !Is0Functor H, !Is0Functor K}
  (alpha : NatEquiv H K) (F : A -> B) `{!Is0Functor F}
  : NatEquiv (H o F) (K o F)
  := Build_NatEquiv' (nattrans_prewhisker alpha F).

Definition natequiv_postwhisker {A B C} {F G : A -> B}
  `{IsGraph A, HasEquivs B, HasEquivs C, !Is0Functor F, !Is0Functor G}
   (K : B -> C) (alpha : NatEquiv F G) `{!Is0Functor K, !Is1Functor K}
  : NatEquiv (K o F) (K o G).A, B, C: Type
F, G: A -> B
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H2: Is1Cat C
H3: HasEquivs C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
K: B -> C
alpha: NatEquiv F G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
NatEquiv (K o F) (K o G)
Proof.A, B, C: Type
F, G: A -> B
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H2: Is1Cat C
H3: HasEquivs C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
K: B -> C
alpha: NatEquiv F G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
NatEquiv (K o F) (K o G)
  srefine (Build_NatEquiv' (nattrans_postwhisker K alpha)).A, B, C: Type
F, G: A -> B
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H2: Is1Cat C
H3: HasEquivs C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
K: B -> C
alpha: NatEquiv F G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
Is1Functor K
A, B, C: Type
F, G: A -> B
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H2: Is1Cat C
H3: HasEquivs C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
K: B -> C
alpha: NatEquiv F G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
forall a : A,
CatIsEquiv (nattrans_postwhisker K alpha a)
  2: unfold nattrans_postwhisker, trans_postwhisker; cbn.A, B, C: Type
F, G: A -> B
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H2: Is1Cat C
H3: HasEquivs C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
K: B -> C
alpha: NatEquiv F G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
Is1Functor K
A, B, C: Type
F, G: A -> B
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H2: Is1Cat C
H3: HasEquivs C
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
K: B -> C
alpha: NatEquiv F G
Is0Functor2: Is0Functor K
Is1Functor0: Is1Functor K
forall a : A, CatIsEquiv (fmap K (alpha a))
  all: exact _.
Defined.

Definition natequiv_inverse {A B : Type} `{IsGraph A} `{HasEquivs B}
  {F G : A -> B} `{!Is0Functor F, !Is0Functor G}
  : NatEquiv F G -> NatEquiv G F.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
NatEquiv F G -> NatEquiv G F
Proof.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
NatEquiv F G -> NatEquiv G F
  intros [alpha I].A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
I: Is1Natural F G (fun a : A => alpha a)
NatEquiv G F
  snrapply Build_NatEquiv.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
I: Is1Natural F G (fun a : A => alpha a)
forall a : A, G a $<~> F a
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
I: Is1Natural F G (fun a : A => alpha a)
Is1Natural G F (fun a : A => ?e a)
  1: intro a; symmetry; apply alpha.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
I: Is1Natural F G (fun a : A => alpha a)
Is1Natural G F
  (fun a : A =>
   (fun a0 : A =>
    symmetric_cate (F a0) (G a0) (alpha a0)) a)
  intros X Y f.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: forall a : A, F a $<~> G a
I: Is1Natural F G (fun a : A => alpha a)
X, Y: A
f: X $-> Y
symmetric_cate (F Y) (G Y) (alpha Y) $o fmap G f $==
fmap F f $o symmetric_cate (F X) (G X) (alpha X)
  apply vinverse, I.
Defined.

(** This lemma might seem unnecessery since as functions ((F o G) o K) and (F o (G o K)) are definitionally equal. But the functor instances of both sides are different. This can be a nasty trap since you cannot see this difference clearly. *)
Definition natequiv_functor_assoc_ff_f {A B C D : Type}
  `{IsGraph A, HasEquivs B, HasEquivs C, HasEquivs D} (** These are a lot of instances... *)
  (F : C -> D) (G : B -> C) (K : A -> B) `{!Is0Functor F, !Is0Functor G, !Is0Functor K}
  : NatEquiv ((F o G) o K) (F o (G o K)).A, B, C, D: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H2: Is1Cat C
H3: HasEquivs C
IsGraph2: IsGraph D
Is2Graph2: Is2Graph D
Is01Cat2: Is01Cat D
H4: Is1Cat D
H5: HasEquivs D
F: C -> D
G: B -> C
K: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
NatEquiv (F o G o K) (F o (G o K))
Proof.A, B, C, D: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H2: Is1Cat C
H3: HasEquivs C
IsGraph2: IsGraph D
Is2Graph2: Is2Graph D
Is01Cat2: Is01Cat D
H4: Is1Cat D
H5: HasEquivs D
F: C -> D
G: B -> C
K: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
NatEquiv (F o G o K) (F o (G o K))
  snrapply Build_NatEquiv.A, B, C, D: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H2: Is1Cat C
H3: HasEquivs C
IsGraph2: IsGraph D
Is2Graph2: Is2Graph D
Is01Cat2: Is01Cat D
H4: Is1Cat D
H5: HasEquivs D
F: C -> D
G: B -> C
K: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
forall a : A,
(fun x : A => (F o G) (K x)) a $<~>
(fun x : A => F ((G o K) x)) a
A, B, C, D: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H2: Is1Cat C
H3: HasEquivs C
IsGraph2: IsGraph D
Is2Graph2: Is2Graph D
Is01Cat2: Is01Cat D
H4: Is1Cat D
H5: HasEquivs D
F: C -> D
G: B -> C
K: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
Is1Natural (fun x : A => (F o G) (K x))
  (fun x : A => F ((G o K) x)) 
  (fun a : A => ?e a)
  1: intro; reflexivity.A, B, C, D: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H2: Is1Cat C
H3: HasEquivs C
IsGraph2: IsGraph D
Is2Graph2: Is2Graph D
Is01Cat2: Is01Cat D
H4: Is1Cat D
H5: HasEquivs D
F: C -> D
G: B -> C
K: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
Is1Natural (fun x : A => (F o G) (K x))
  (fun x : A => F ((G o K) x))
  (fun a : A =>
   (fun a0 : A => reflexive_cate (F (G (K a0)))) a)
  intros X Y f.A, B, C, D: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H2: Is1Cat C
H3: HasEquivs C
IsGraph2: IsGraph D
Is2Graph2: Is2Graph D
Is01Cat2: Is01Cat D
H4: Is1Cat D
H5: HasEquivs D
F: C -> D
G: B -> C
K: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
X, Y: A
f: X $-> Y
reflexive_cate (F (G (K Y))) $o
fmap ((fun x : B => F (G x)) o K) f $==
fmap (F o (fun x : A => G (K x))) f $o
reflexive_cate (F (G (K X)))
  refine (cat_prewhisker (id_cate_fun _) _ $@ cat_idl _ $@ _^$).A, B, C, D: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
H1: HasEquivs B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H2: Is1Cat C
H3: HasEquivs C
IsGraph2: IsGraph D
Is2Graph2: Is2Graph D
Is01Cat2: Is01Cat D
H4: Is1Cat D
H5: HasEquivs D
F: C -> D
G: B -> C
K: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
Is0Functor2: Is0Functor K
X, Y: A
f: X $-> Y
fmap (F o (fun x : A => G (K x))) f $o
reflexive_cate (F (G (K X))) $->
fmap ((fun x : B => F (G x)) o K) f
  refine (cat_postwhisker _ (id_cate_fun _) $@ cat_idr _).
Defined.

Lemma natequiv_op {A B : Type} `{Is01Cat A} `{HasEquivs B}
  (F G : A -> B) `{!Is0Functor F, !Is0Functor G}
  : NatEquiv F G -> NatEquiv (G : A^op -> B^op) F.A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
NatEquiv F G -> NatEquiv (G : A^op -> B^op) F
Proof.A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
NatEquiv F G -> NatEquiv (G : A^op -> B^op) F
  intros [a n].A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
a: forall a : A, F a $<~> G a
n: Is1Natural F G (fun a0 : A => a a0)
NatEquiv G F
  snrapply Build_NatEquiv.A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
a: forall a : A, F a $<~> G a
n: Is1Natural F G (fun a0 : A => a a0)
forall a : A^op, G a $<~> F a
A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
a: forall a : A, F a $<~> G a
n: Is1Natural F G (fun a0 : A => a a0)
Is1Natural G F (fun a0 : A^op => ?e a0)
  1: exact a.A, B: Type
H: IsGraph A
H0: Is01Cat A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
a: forall a : A, F a $<~> G a
n: Is1Natural F G (fun a0 : A => a a0)
Is1Natural G F (fun a0 : A^op => a a0)
  rapply is1nat_op.
Defined.

(** *** Pointed natural transformations *)

Definition PointedTransformation {B C : Type} `{Is1Cat B, Is1Gpd C}
           `{IsPointed B, IsPointed C} (F G : B -->* C)
  := {eta : F $=> G & eta (point _) $== bp_pointed F $@ (bp_pointed G)^$}.

Notation "F $=>* G" := (PointedTransformation F G) (at level 70).

Definition ptransformation_inverse {B C : Type} `{Is1Cat B, Is1Gpd C}
           `{IsPointed B, IsPointed C} (F G : B -->* C)
  : (F $=>* G) -> (G $=>* F).B, C: Type
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H0: Is1Cat C
Is0Gpd0: Is0Gpd C
H1: Is1Gpd C
H2: IsPointed B
H3: IsPointed C
F, G: B -->* C
F $=>* G -> G $=>* F
Proof.B, C: Type
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H0: Is1Cat C
Is0Gpd0: Is0Gpd C
H1: Is1Gpd C
H2: IsPointed B
H3: IsPointed C
F, G: B -->* C
F $=>* G -> G $=>* F
  intros [h p].B, C: Type
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H0: Is1Cat C
Is0Gpd0: Is0Gpd C
H1: Is1Gpd C
H2: IsPointed B
H3: IsPointed C
F, G: B -->* C
h: F $=> G
p: h (point B) $== bp_pointed F $@ (bp_pointed G)^$
G $=>* F
  exists (fun x => (h x)^$).B, C: Type
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H0: Is1Cat C
Is0Gpd0: Is0Gpd C
H1: Is1Gpd C
H2: IsPointed B
H3: IsPointed C
F, G: B -->* C
h: F $=> G
p: h (point B) $== bp_pointed F $@ (bp_pointed G)^$
(h (point B))^$ $== bp_pointed G $@ (bp_pointed F)^$
  refine (gpd_rev2 p $@ _).B, C: Type
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H0: Is1Cat C
Is0Gpd0: Is0Gpd C
H1: Is1Gpd C
H2: IsPointed B
H3: IsPointed C
F, G: B -->* C
h: F $=> G
p: h (point B) $== bp_pointed F $@ (bp_pointed G)^$
(bp_pointed F $@ (bp_pointed G)^$)^$ $==
bp_pointed G $@ (bp_pointed F)^$
  refine (gpd_rev_pp _ _ $@ _).B, C: Type
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H0: Is1Cat C
Is0Gpd0: Is0Gpd C
H1: Is1Gpd C
H2: IsPointed B
H3: IsPointed C
F, G: B -->* C
h: F $=> G
p: h (point B) $== bp_pointed F $@ (bp_pointed G)^$
(bp_pointed F)^$ $o ((bp_pointed G)^$)^$ $==
bp_pointed G $@ (bp_pointed F)^$
  refine (_ $@L _).B, C: Type
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H0: Is1Cat C
Is0Gpd0: Is0Gpd C
H1: Is1Gpd C
H2: IsPointed B
H3: IsPointed C
F, G: B -->* C
h: F $=> G
p: h (point B) $== bp_pointed F $@ (bp_pointed G)^$
((bp_pointed G)^$)^$ $== bp_pointed G
  apply gpd_rev_rev.
Defined.

Notation "h ^*$" := (ptransformation_inverse _ _ h) (at level 5).

Definition ptransformation_compose {B C : Type} `{Is1Cat B, Is1Gpd C}
           `{IsPointed B, IsPointed C} {F0 F1 F2 : B -->* C}
  : (F0 $=>* F1) -> (F1 $=>* F2) -> (F0 $=>* F2).B, C: Type
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H0: Is1Cat C
Is0Gpd0: Is0Gpd C
H1: Is1Gpd C
H2: IsPointed B
H3: IsPointed C
F0, F1, F2: B -->* C
F0 $=>* F1 -> F1 $=>* F2 -> F0 $=>* F2
Proof.B, C: Type
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H0: Is1Cat C
Is0Gpd0: Is0Gpd C
H1: Is1Gpd C
H2: IsPointed B
H3: IsPointed C
F0, F1, F2: B -->* C
F0 $=>* F1 -> F1 $=>* F2 -> F0 $=>* F2
  intros [h0 p0] [h1 p1].B, C: Type
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H0: Is1Cat C
Is0Gpd0: Is0Gpd C
H1: Is1Gpd C
H2: IsPointed B
H3: IsPointed C
F0, F1, F2: B -->* C
h0: F0 $=> F1
p0: h0 (point B) $==
bp_pointed F0 $@ (bp_pointed F1)^$
h1: F1 $=> F2
p1: h1 (point B) $==
bp_pointed F1 $@ (bp_pointed F2)^$
F0 $=>* F2
  exists (trans_comp h1 h0).B, C: Type
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H0: Is1Cat C
Is0Gpd0: Is0Gpd C
H1: Is1Gpd C
H2: IsPointed B
H3: IsPointed C
F0, F1, F2: B -->* C
h0: F0 $=> F1
p0: h0 (point B) $==
bp_pointed F0 $@ (bp_pointed F1)^$
h1: F1 $=> F2
p1: h1 (point B) $==
bp_pointed F1 $@ (bp_pointed F2)^$
trans_comp h1 h0 (point B) $==
bp_pointed F0 $@ (bp_pointed F2)^$
  refine ((p1 $@R _) $@ (_ $@L p0) $@ _);
    unfold gpd_comp; cbn.B, C: Type
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H0: Is1Cat C
Is0Gpd0: Is0Gpd C
H1: Is1Gpd C
H2: IsPointed B
H3: IsPointed C
F0, F1, F2: B -->* C
h0: F0 $=> F1
p0: h0 (point B) $==
bp_pointed F0 $@ (bp_pointed F1)^$
h1: F1 $=> F2
p1: h1 (point B) $==
bp_pointed F1 $@ (bp_pointed F2)^$
(bp_pointed F2)^$ $o bp_pointed F1 $o
((bp_pointed F1)^$ $o bp_pointed F0) $==
(bp_pointed F2)^$ $o bp_pointed F0
  refine (cat_assoc _ _ _ $@ _).B, C: Type
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H0: Is1Cat C
Is0Gpd0: Is0Gpd C
H1: Is1Gpd C
H2: IsPointed B
H3: IsPointed C
F0, F1, F2: B -->* C
h0: F0 $=> F1
p0: h0 (point B) $==
bp_pointed F0 $@ (bp_pointed F1)^$
h1: F1 $=> F2
p1: h1 (point B) $==
bp_pointed F1 $@ (bp_pointed F2)^$
(bp_pointed F2)^$ $o
(bp_pointed F1 $o ((bp_pointed F1)^$ $o bp_pointed F0)) $==
(bp_pointed F2)^$ $o bp_pointed F0
  rapply (fmap _).B, C: Type
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H: Is1Cat B
IsGraph1: IsGraph C
Is2Graph1: Is2Graph C
Is01Cat1: Is01Cat C
H0: Is1Cat C
Is0Gpd0: Is0Gpd C
H1: Is1Gpd C
H2: IsPointed B
H3: IsPointed C
F0, F1, F2: B -->* C
h0: F0 $=> F1
p0: h0 (point B) $==
bp_pointed F0 $@ (bp_pointed F1)^$
h1: F1 $=> F2
p1: h1 (point B) $==
bp_pointed F1 $@ (bp_pointed F2)^$
bp_pointed F1 $o ((bp_pointed F1)^$ $o bp_pointed F0) $->
bp_pointed F0
  apply gpd_h_Vh.
Defined.

Notation "h $@* k" := (ptransformation_compose h k) (at level 40).

(* TODO: *)
(* Morphisms of natural transformations - Modifications *)
(* Since [Transformation] is dependent, we can define a modification to be a transformation together with a cylinder condition. This doesn't seem to be too useful as of yet however. We would also need better ways to write down cylinders. *)