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.

(** * Wild Natural Transformations *)

(** ** Transformations *)

(** *** Definition *)

(** A transformation is simply a family of 1-cells over some base type [A] between the sections of two dependent functions [F] and [G]. In most cases [F] and [G] will be non-dependent functors. *)
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).

(** The identity transformation between a functor and itself is the identity function at the section. *)
Definition trans_id {A B : Type} `{Is01Cat B} (F : A -> B)
  : F $=> F
  := fun a => Id (F a).

(** Transformations can be composed pointwise. *)
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.

(** Transformations can be prewhiskered by a function. This means we precompose both sides of the transformation with a function. *)
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.

(** Transformations can be postwhiskered by a function. This means we postcompose both sides of the transformation with a function. *)
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).

(** A transformation in the opposite category is simply a transformation in the original category with the direction swapped. *)
Definition trans_op {A} {B} `{Is01Cat B}
  (F : A -> B) (G : A -> B) (alpha : F $=> G)
  : Transformation (A:=A^op) (B:=fun _ => B^op) G (F : A^op -> B^op)
  := alpha.

(** ** Naturality *)

(** A transformation is 1-natural if there exists a 2-cell witnessing the naturality square. The codomain of the transformation must be a wild 1-category. *)
Class Is1Natural {A B : Type} `{IsGraph A, Is1Cat B}
  (F : A -> B) `{!Is0Functor F} (G : A -> B) `{!Is0Functor G}
  (alpha : F $=> G) := Build_Is1Natural' {
  isnat {a a'} (f : a $-> a') : alpha a' $o fmap F f $== fmap G f $o alpha a;
  (** We also include the transposed naturality square in the definition so that opposite natural transformations are definitionally involutive. In most cases, this will be constructed to be the inverse of the [isnat] field. *)
  isnat_tr {a a'} (f : a $-> a') : fmap G f $o alpha a $== alpha a' $o fmap F f;
}.

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.
Arguments isnat_tr {_ _ _ _ _ _ _ _ _ _ _} alpha {alnat _ _} f : rename.

(** We coerce naturality proofs to their naturality square as the [isnat] projection can be unwieldy in certain situations where the transformation is difficult to write down. This allows for the naturality proof to be used directly. *)
Coercion isnat : Is1Natural >-> Funclass.

Definition Build_Is1Natural {A B : Type} `{IsGraph A} `{Is1Cat B}
  {F G : A -> B} `{!Is0Functor F, !Is0Functor G} (alpha : F $=> G)
  (isnat : forall a a' (f : a $-> a'), alpha a' $o fmap F f $== fmap G f $o alpha a)
  : Is1Natural F G alpha.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: F $=> G
isnat: forall (a a' : A) (f : a $-> a'),
alpha a' $o fmap F f $== fmap G f $o alpha a
Is1Natural F G alpha
Proof.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: F $=> G
isnat: forall (a a' : A) (f : a $-> a'),
alpha a' $o fmap F f $== fmap G f $o alpha a
Is1Natural F G alpha
  snapply Build_Is1Natural'.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: F $=> G
isnat: forall (a a' : A) (f : a $-> a'),
alpha a' $o fmap F f $== fmap G f $o alpha a
forall (a a' : A) (f : a $-> a'),
alpha a' $o fmap F f $== fmap G f $o alpha a
A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: F $=> G
isnat: forall (a a' : A) (f : a $-> a'),
alpha a' $o fmap F f $== fmap G f $o alpha a
forall (a a' : A) (f : a $-> a'),
fmap G f $o alpha a $== alpha a' $o fmap F f
  -A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: F $=> G
isnat: forall (a a' : A) (f : a $-> a'),
alpha a' $o fmap F f $== fmap G f $o alpha a
forall (a a' : A) (f : a $-> a'),
alpha a' $o fmap F f $== fmap G f $o alpha a exact isnat.
  -A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: F $=> G
isnat: forall (a a' : A) (f : a $-> a'),
alpha a' $o fmap F f $== fmap G f $o alpha a
forall (a a' : A) (f : a $-> a'),
fmap G f $o alpha a $== alpha a' $o fmap F f intros a a' f.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F, G: A -> B
Is0Functor0: Is0Functor F
Is0Functor1: Is0Functor G
alpha: F $=> G
isnat: forall (a a' : A) (f : a $-> a'),
alpha a' $o fmap F f $== fmap G f $o alpha a
a, a': A
f: a $-> a'
fmap G f $o alpha a $== alpha a' $o fmap F f
    exact (isnat a a' f)^$.
Defined.

(** The identity transformation is 1-natural. *)
Instance is1natural_id {A B : Type} `{IsGraph A} `{Is1Cat B}
  (F : A -> B) `{!Is0Functor F}
  : Is1Natural F F (trans_id 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 (trans_id 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 (trans_id F)
  snapply Build_Is1Natural.A, B: Type
H: IsGraph A
IsGraph0: IsGraph B
Is2Graph0: Is2Graph B
Is01Cat0: Is01Cat B
H0: Is1Cat B
F: A -> B
Is0Functor0: Is0Functor F
forall (a a' : A) (f : a $-> a'),
trans_id F a' $o fmap F f $== fmap F f $o trans_id F a
  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
trans_id F b $o fmap F f $== fmap F f $o trans_id F a
  exact (cat_idl _ $@ (cat_idr _)^$).
Defined.

(** The composite of 1-natural transformations is 1-natural. *)
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)
  snapply Build_Is1Natural.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
forall (a a' : A) (f : a $-> a'),
trans_comp gamma alpha a' $o fmap F f $==
fmap K f $o trans_comp gamma alpha a
  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.

(** Prewhiskering a transformation preserves naturality. *)
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)
  snapply Build_Is1Natural.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
forall (a a' : A) (f : a $-> a'),
trans_prewhisker gamma K a' $o fmap (F o K) f $==
fmap (G o K) f $o trans_prewhisker gamma K a
  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 (isnat gamma _).
Defined.

(** Postwhiskering a transformation preserves naturality. *)
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)
  snapply Build_Is1Natural.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
forall (a a' : A) (f : a $-> a'),
trans_postwhisker K gamma a' $o fmap (K o F) f $==
fmap (K o G) f $o trans_postwhisker K gamma a
  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 (isnat gamma _).
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
  snapply Build_Is1Natural.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
forall (a a' : A) (f : a $-> a'),
alpha a' $o fmap F f $== fmap G f $o 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, 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.

(** The opposite of a natural transformation is natural. *)
Instance is1natural_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) (trans_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)
  (trans_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)
  (trans_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 (trans_op F G alpha)
  snapply Build_Is1Natural'.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
forall (a a' : A) (f : a $-> a'),
trans_op F G alpha a' $o fmap (G : A^op -> B^op) f $==
fmap (F : A^op -> B^op) f $o trans_op F G alpha a
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
forall (a a' : A) (f : a $-> a'),
fmap (F : A^op -> B^op) f $o trans_op F G alpha a $==
trans_op F G alpha a' $o fmap (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
F: A -> B
Is0Functor0: Is0Functor F
G: A -> B
Is0Functor1: Is0Functor G
alpha: F $=> G
Is1Natural0: Is1Natural F G alpha
forall (a a' : A) (f : a $-> a'),
trans_op F G alpha a' $o fmap (G : A^op -> B^op) f $==
fmap (F : A^op -> B^op) f $o trans_op F G alpha a intros a b.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
forall f : a $-> b,
trans_op F G alpha b $o fmap (G : A^op -> B^op) f $==
fmap (F : A^op -> B^op) f $o trans_op F G alpha a
    exact (isnat_tr 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
forall (a a' : A) (f : a $-> a'),
fmap (F : A^op -> B^op) f $o trans_op F G alpha a $==
trans_op F G alpha a' $o fmap (G : A^op -> B^op) f intros a b.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
forall f : a $-> b,
fmap (F : A^op -> B^op) f $o trans_op F G alpha a $==
trans_op F G alpha b $o fmap (G : A^op -> B^op) f
    exact (isnat alpha).
Defined.

(** ** Natural transformations *)

(** Here we give the bundled definition of a natural transformation which can be more convenient to work with in certain situations. It forms the Hom type of the functor category. *)

Record NatTrans {A B : Type} `{IsGraph A} `{Is1Cat B} {F G : A -> B}
  {ff : Is0Functor F} {fg : Is0Functor G} := {
  #[reversible=no]
  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.

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

Definition nattrans_id {A B : Type} (F : A -> B)
  `{IsGraph A, Is1Cat B, !Is0Functor F}
  : NatTrans F F
  := Build_NatTrans (trans_id F) _.

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
  := fun alpha beta => Build_NatTrans (trans_comp alpha beta) _.

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)
  := Build_NatTrans (trans_prewhisker alpha K) _.

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)
  := fun alpha => Build_NatTrans (trans_postwhisker K alpha) _.

Definition nattrans_op {A B : Type} `{Is01Cat A} `{Is1Cat B}
  {F G : A -> B} `{!Is0Functor F, !Is0Functor G}
  : NatTrans F G
    -> NatTrans (A:=A^op) (B:=B^op) (G : A^op -> B^op) (F : A^op -> B^op)
  := fun alpha => Build_NatTrans (trans_op F G alpha) _.

(** ** Natural equivalences *)

(** Natural equivalences are families of equivalences that are natural. *)
Record NatEquiv {A B : Type} `{IsGraph A} `{HasEquivs B}
  {F G : A -> B} `{!Is0Functor F, !Is0Functor G} := {
  #[reversible=no]
  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).

(** From a given natural equivalence, we can get the underlying natural transformation. *)
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
  napply 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
  exact (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 sometimes 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.

(** Often we wish to build a natural equivalence from a natural transformation and a pointwise proof that it is an equivalence. *)
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
  snapply 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
    exact (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) snapply Build_Is1Natural'.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' : A) (f : a $-> a'),
(fun a0 : A =>
 cate_fun
   ((fun a1 : A => Build_CatEquiv (alpha a1)) a0)) a' $o
fmap F f $==
fmap G f $o
(fun a0 : A =>
 cate_fun
   ((fun a1 : A => Build_CatEquiv (alpha a1)) a0)) 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' : A) (f : a $-> a'),
fmap G f $o
(fun a0 : A =>
 cate_fun
   ((fun a1 : A => Build_CatEquiv (alpha a1)) a0)) a $==
(fun a0 : A =>
 cate_fun
   ((fun a1 : A => Build_CatEquiv (alpha a1)) a0)) a' $o
fmap F 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)
forall (a a' : A) (f : a $-> a'),
(fun a0 : A =>
 cate_fun
   ((fun a1 : A => Build_CatEquiv (alpha a1)) a0)) a' $o
fmap F f $==
fmap G f $o
(fun a0 : A =>
 cate_fun
   ((fun a1 : A => Build_CatEquiv (alpha a1)) 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'
(fun a : A =>
 cate_fun
   ((fun a0 : A => Build_CatEquiv (alpha a0)) a)) a' $o
fmap F f $==
fmap G f $o
(fun a : A =>
 cate_fun
   ((fun a0 : A => Build_CatEquiv (alpha a0)) a)) 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
      exact (isnat 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: NatTrans F G
H2: forall a : A, CatIsEquiv (alpha a)
forall (a a' : A) (f : a $-> a'),
fmap G f $o
(fun a0 : A =>
 cate_fun
   ((fun a1 : A => Build_CatEquiv (alpha a1)) a0)) a $==
(fun a0 : A =>
 cate_fun
   ((fun a1 : A => Build_CatEquiv (alpha a1)) a0)) a' $o
fmap F f 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'
fmap G f $o
(fun a : A =>
 cate_fun
   ((fun a0 : A => Build_CatEquiv (alpha a0)) a)) a $==
(fun a : A =>
 cate_fun
   ((fun a0 : A => Build_CatEquiv (alpha a0)) a)) a' $o
fmap F f
      refine ((_ $@L cate_buildequiv_fun _) $@ _ $@ (cate_buildequiv_fun _ $@R _)^$).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'
fmap G f $o alpha a $== alpha a' $o fmap F f
      exact (isnat_tr alpha _).
Defined.

Definition natequiv_id {A B : Type} `{IsGraph A} `{HasEquivs B}
  {F : A -> B} `{!Is0Functor F}
  : NatEquiv F F
  := Build_NatEquiv' (nattrans_id F).

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.

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
  snapply 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)
  by rapply is1natural_op.
Defined.

(** We can form the inverse natural equivalence by inverting each map in the family. The naturality proof follows from standard lemmas about inverses. *)
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
  snapply 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: exact (fun a => (alpha a)^-1$).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 => (alpha a0)^-1$) a)
  snapply Build_Is1Natural'.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' : A) (f : a $-> a'),
(fun a0 : A =>
 cate_fun ((fun a1 : A => (alpha a1)^-1$) a0)) a' $o
fmap G f $==
fmap F f $o
(fun a0 : A =>
 cate_fun ((fun a1 : A => (alpha a1)^-1$) a0)) 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)
forall (a a' : A) (f : a $-> a'),
fmap F f $o
(fun a0 : A =>
 cate_fun ((fun a1 : A => (alpha a1)^-1$) a0)) a $==
(fun a0 : A =>
 cate_fun ((fun a1 : A => (alpha a1)^-1$) a0)) a' $o
fmap 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
alpha: forall a : A, F a $<~> G a
I: Is1Natural F G (fun a : A => alpha a)
forall (a a' : A) (f : a $-> a'),
(fun a0 : A =>
 cate_fun ((fun a1 : A => (alpha a1)^-1$) a0)) a' $o
fmap G f $==
fmap F f $o
(fun a0 : A =>
 cate_fun ((fun a1 : A => (alpha a1)^-1$) 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
(fun a : A =>
 cate_fun ((fun a0 : A => (alpha a0)^-1$) a)) Y $o
fmap G f $==
fmap F f $o
(fun a : A =>
 cate_fun ((fun a0 : A => (alpha a0)^-1$) a)) X
    apply vinverse, 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)
forall (a a' : A) (f : a $-> a'),
fmap F f $o
(fun a0 : A =>
 cate_fun ((fun a1 : A => (alpha a1)^-1$) a0)) a $==
(fun a0 : A =>
 cate_fun ((fun a1 : A => (alpha a1)^-1$) a0)) a' $o
fmap G f 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
fmap F f $o
(fun a : A =>
 cate_fun ((fun a0 : A => (alpha a0)^-1$) a)) X $==
(fun a : A =>
 cate_fun ((fun a0 : A => (alpha a0)^-1$) a)) Y $o
fmap G f
    apply hinverse, I.
Defined.

(** This lemma might seem unnecessary 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} 
  (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))
  snapply 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)
  snapply Build_Is1Natural.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' : A) (f : a $-> a'),
(fun a0 : A =>
 cate_fun
   ((fun a1 : A => reflexive_cate (F (G (K a1)))) a0))
  a' $o fmap ((fun x : B => F (G x)) o K) f $==
fmap (F o (fun x : A => G (K x))) f $o
(fun a0 : A =>
 cate_fun
   ((fun a1 : A => reflexive_cate (F (G (K a1)))) 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
(fun a : A =>
 cate_fun
   ((fun a0 : A => reflexive_cate (F (G (K a0)))) a))
  Y $o fmap ((fun x : B => F (G x)) o K) f $==
fmap (F o (fun x : A => G (K x))) f $o
(fun a : A =>
 cate_fun
   ((fun a0 : A => reflexive_cate (F (G (K a0)))) a))
  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
  exact (cat_postwhisker _ (id_cate_fun _) $@ cat_idr _).
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. *)