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

(** * Bifunctors between WildCats *)

(** ** Definition *)

(** We choose to store redundant information in the class, so that depending on how an instance is constructed, we will get the expected implementations of [fmap10], [fmap01] and [fmap11]. *)
Class Is0Bifunctor {A B C : Type}
  `{IsGraph A, IsGraph B, IsGraph C} (F : A -> B -> C) := {
  is0functor_bifunctor_uncurried :: Is0Functor (uncurry F);
  is0functor01_bifunctor :: forall a, Is0Functor (F a);
  is0functor10_bifunctor :: forall b, Is0Functor (flip F b);
}.

Arguments Is0Bifunctor {A B C _ _ _} F.
Arguments is0functor_bifunctor_uncurried {A B C _ _ _} F {_}.
Arguments is0functor01_bifunctor {A B C _ _ _} F {_} a : rename.
Arguments is0functor10_bifunctor {A B C _ _ _} F {_} b : rename.

(** We provide two alternate constructors, allowing the user to provide just the first field or the last two fields. *)
Definition Build_Is0Bifunctor' {A B C : Type}
  `{Is01Cat A, Is01Cat B, IsGraph C} (F : A -> B -> C)
  `{!Is0Functor (uncurry F)}
  : Is0Bifunctor F.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
H3: IsGraph C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is0Bifunctor F
Proof.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
H3: IsGraph C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is0Bifunctor F
  snapply Build_Is0Bifunctor.
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
H3: IsGraph C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is0Functor (uncurry F)
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
H3: IsGraph C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
forall a : A, Is0Functor (F a)
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
H3: IsGraph C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
forall b : B, Is0Functor (flip F b)
  -
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
H3: IsGraph C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is0Functor (uncurry F) exact _.
  -
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
H3: IsGraph C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
forall a : A, Is0Functor (F a) exact (is0functor_functor_uncurried01 (uncurry F)).
  -
A, B, C: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
H3: IsGraph C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
forall b : B, Is0Functor (flip F b) exact (is0functor_functor_uncurried10 (uncurry F)).
Defined.

Definition Build_Is0Bifunctor'' {A B C : Type}
  `{IsGraph A, IsGraph B, Is01Cat C} (F : A -> B -> C)
  `{!forall a, Is0Functor (F a), !forall b, Is0Functor (flip F b)}
  : Is0Bifunctor F.
A, B, C: Type
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: Is01Cat C
F: A -> B -> C
H3: forall a : A, Is0Functor (F a)
H4: forall b : B, Is0Functor (flip F b)
Is0Bifunctor F
Proof.
A, B, C: Type
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: Is01Cat C
F: A -> B -> C
H3: forall a : A, Is0Functor (F a)
H4: forall b : B, Is0Functor (flip F b)
Is0Bifunctor F
  (* The first condition follows from [is0functor_prod_is0functor]. *)
  napply Build_Is0Bifunctor; exact _.
Defined.

(** *** 1-functorial action *)

(** [fmap] in the first argument. *)
Definition fmap10 {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
  (F : A -> B -> C) `{!Is0Bifunctor F} {a0 a1 : A} (f : a0 $-> a1) (b : B)
  : (F a0 b) $-> (F a1 b)
  := fmap (flip F b) f.

(** [fmap] in the second argument. *)
Definition fmap01 {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
  (F : A -> B -> C) `{!Is0Bifunctor F} (a : A) {b0 b1 : B} (g : b0 $-> b1)
  : F a b0 $-> F a b1
  := fmap (F a) g.

(** [fmap] in both arguments. *)
Definition fmap11 {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
  (F : A -> B -> C) `{!Is0Bifunctor F} {a0 a1 : A} (f : a0 $-> a1)
  {b0 b1 : B} (g : b0 $-> b1)
  : F a0 b0 $-> F a1 b1
  := fmap_pair (uncurry F) f g.

(** As with [Is0Bifunctor], we store redundant information.  In addition, we store the proofs that they are consistent with each other. *)
Class Is1Bifunctor {A B C : Type}
  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C) `{!Is0Bifunctor F} := {

  is1functor_bifunctor_uncurried :: Is1Functor (uncurry F);
  is1functor01_bifunctor :: forall a, Is1Functor (F a);
  is1functor10_bifunctor :: forall b, Is1Functor (flip F b);

  fmap11_is_fmap01_fmap10 {a0 a1} (f : a0 $-> a1) {b0 b1} (g : b0 $-> b1)
    : fmap11 F f g $== fmap01 F a1 g $o fmap10 F f b0;
  fmap11_is_fmap10_fmap01 {a0 a1} (f : a0 $-> a1) {b0 b1} (g : b0 $-> b1)
    : fmap11 F f g $== fmap10 F f b1 $o fmap01 F a0 g;
}.

Arguments Is1Bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {Is0Bifunctor} : rename.
Arguments Build_Is1Bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {_} _ _ _ _ _.
Arguments is1functor_bifunctor_uncurried {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {_ _}.
Arguments is1functor01_bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {_ _} a : rename.
Arguments is1functor10_bifunctor {A B C _ _ _ _ _ _ _ _ _ _ _ _} F {_ _} b : rename.
Arguments fmap11_is_fmap01_fmap10 {A B C _ _ _ _ _ _ _ _ _ _ _ _} F
  {Is0Bifunctor Is1Bifunctor} {a0 a1} f {b0 b1} g : rename.
Arguments fmap11_is_fmap10_fmap01 {A B C _ _ _ _ _ _ _ _ _ _ _ _} F
  {Is0Bifunctor Is1Bifunctor} {a0 a1} f {b0 b1} g : rename.

(** We again provide two alternate constructors. *)
Definition Build_Is1Bifunctor' {A B C : Type}
  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
  `{!Is0Functor (uncurry F), !Is1Functor (uncurry F)}
  : Is1Bifunctor (Is0Bifunctor := Build_Is0Bifunctor' F) F.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is1Functor0: Is1Functor (uncurry F)
Is1Bifunctor F
Proof.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is1Functor0: Is1Functor (uncurry F)
Is1Bifunctor F
  snapply Build_Is1Bifunctor.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is1Functor0: Is1Functor (uncurry F)
Is1Functor (uncurry F)
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is1Functor0: Is1Functor (uncurry F)
forall a : A, Is1Functor (F a)
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is1Functor0: Is1Functor (uncurry F)
forall b : B, Is1Functor (flip F b)
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is1Functor0: Is1Functor (uncurry F)
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : B) (g : b0 $-> b1),
fmap11 F f g $== fmap01 F a1 g $o fmap10 F f b0
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is1Functor0: Is1Functor (uncurry F)
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : B) (g : b0 $-> b1),
fmap11 F f g $== fmap10 F f b1 $o fmap01 F a0 g
  -
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is1Functor0: Is1Functor (uncurry F)
Is1Functor (uncurry F) exact _.
  -
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is1Functor0: Is1Functor (uncurry F)
forall a : A, Is1Functor (F a) exact (is1functor_functor_uncurried01 (uncurry F)).
  -
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is1Functor0: Is1Functor (uncurry F)
forall b : B, Is1Functor (flip F b) exact (is1functor_functor_uncurried10 (uncurry F)).
  -
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is1Functor0: Is1Functor (uncurry F)
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : B) (g : b0 $-> b1),
fmap11 F f g $== fmap01 F a1 g $o fmap10 F f b0 intros a0 a1 f b0 b1 g.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is1Functor0: Is1Functor (uncurry F)
a0, a1: A
f: a0 $-> a1
b0, b1: B
g: b0 $-> b1
fmap11 F f g $== fmap01 F a1 g $o fmap10 F f b0
    refine (_^$ $@ fmap_pair_comp (uncurry F) f (Id b0) (Id a1) g).
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is1Functor0: Is1Functor (uncurry F)
a0, a1: A
f: a0 $-> a1
b0, b1: B
g: b0 $-> b1
fmap_pair (uncurry F) (Id a1 $o f) (g $o Id b0) $->
fmap11 F f g
    exact (fmap2_pair (uncurry F) (cat_idl _) (cat_idr _)).
  -
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is1Functor0: Is1Functor (uncurry F)
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : B) (g : b0 $-> b1),
fmap11 F f g $== fmap10 F f b1 $o fmap01 F a0 g intros a0 a1 f b0 b1 g.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is1Functor0: Is1Functor (uncurry F)
a0, a1: A
f: a0 $-> a1
b0, b1: B
g: b0 $-> b1
fmap11 F f g $== fmap10 F f b1 $o fmap01 F a0 g
    refine (_^$ $@ fmap_pair_comp (uncurry F) (Id a0) g f (Id b1)).
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Functor0: Is0Functor (uncurry F)
Is1Functor0: Is1Functor (uncurry F)
a0, a1: A
f: a0 $-> a1
b0, b1: B
g: b0 $-> b1
fmap_pair (uncurry F) (f $o Id a0) (Id b1 $o g) $->
fmap11 F f g
    exact (fmap2_pair (uncurry F) (cat_idr _) (cat_idl _)).
Defined.

Definition Build_Is1Bifunctor'' {A B C : Type}
  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C)
  `{!forall a, Is0Functor (F a), !forall b, Is0Functor (flip F b)}
  (Is0Bifunctor_F := Build_Is0Bifunctor'' F)
  `{!forall a, Is1Functor (F a), !forall b, Is1Functor (flip F b)}
  (bifunctor_coh : forall a0 a1 (f : a0 $-> a1) b0 b1 (g : b0 $-> b1),
    fmap01 F a1 g $o fmap10 F f b0 $== fmap10 F f b1 $o fmap01 F a0 g)
  : Is1Bifunctor F.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
H2: forall a : A, Is0Functor (F a)
H3: forall b : B, Is0Functor (flip F b)
Is0Bifunctor_F:= Build_Is0Bifunctor'' F: Is0Bifunctor F
H4: forall a : A, Is1Functor (F a)
H5: forall b : B, Is1Functor (flip F b)
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap01 F a1 g $o fmap10 F f b0 $==
fmap10 F f b1 $o fmap01 F a0 g
Is1Bifunctor F
Proof.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
H2: forall a : A, Is0Functor (F a)
H3: forall b : B, Is0Functor (flip F b)
Is0Bifunctor_F:= Build_Is0Bifunctor'' F: Is0Bifunctor F
H4: forall a : A, Is1Functor (F a)
H5: forall b : B, Is1Functor (flip F b)
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap01 F a1 g $o fmap10 F f b0 $==
fmap10 F f b1 $o fmap01 F a0 g
Is1Bifunctor F
  snapply Build_Is1Bifunctor.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
H2: forall a : A, Is0Functor (F a)
H3: forall b : B, Is0Functor (flip F b)
Is0Bifunctor_F:= Build_Is0Bifunctor'' F: Is0Bifunctor F
H4: forall a : A, Is1Functor (F a)
H5: forall b : B, Is1Functor (flip F b)
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap01 F a1 g $o fmap10 F f b0 $==
fmap10 F f b1 $o fmap01 F a0 g
Is1Functor (uncurry F)
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
H2: forall a : A, Is0Functor (F a)
H3: forall b : B, Is0Functor (flip F b)
Is0Bifunctor_F:= Build_Is0Bifunctor'' F: Is0Bifunctor F
H4: forall a : A, Is1Functor (F a)
H5: forall b : B, Is1Functor (flip F b)
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap01 F a1 g $o fmap10 F f b0 $==
fmap10 F f b1 $o fmap01 F a0 g
forall a : A, Is1Functor (F a)
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
H2: forall a : A, Is0Functor (F a)
H3: forall b : B, Is0Functor (flip F b)
Is0Bifunctor_F:= Build_Is0Bifunctor'' F: Is0Bifunctor F
H4: forall a : A, Is1Functor (F a)
H5: forall b : B, Is1Functor (flip F b)
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap01 F a1 g $o fmap10 F f b0 $==
fmap10 F f b1 $o fmap01 F a0 g
forall b : B, Is1Functor (flip F b)
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
H2: forall a : A, Is0Functor (F a)
H3: forall b : B, Is0Functor (flip F b)
Is0Bifunctor_F:= Build_Is0Bifunctor'' F: Is0Bifunctor F
H4: forall a : A, Is1Functor (F a)
H5: forall b : B, Is1Functor (flip F b)
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap01 F a1 g $o fmap10 F f b0 $==
fmap10 F f b1 $o fmap01 F a0 g
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : B) (g : b0 $-> b1),
fmap11 F f g $== fmap01 F a1 g $o fmap10 F f b0
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
H2: forall a : A, Is0Functor (F a)
H3: forall b : B, Is0Functor (flip F b)
Is0Bifunctor_F:= Build_Is0Bifunctor'' F: Is0Bifunctor F
H4: forall a : A, Is1Functor (F a)
H5: forall b : B, Is1Functor (flip F b)
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap01 F a1 g $o fmap10 F f b0 $==
fmap10 F f b1 $o fmap01 F a0 g
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : B) (g : b0 $-> b1),
fmap11 F f g $== fmap10 F f b1 $o fmap01 F a0 g
  -
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
H2: forall a : A, Is0Functor (F a)
H3: forall b : B, Is0Functor (flip F b)
Is0Bifunctor_F:= Build_Is0Bifunctor'' F: Is0Bifunctor F
H4: forall a : A, Is1Functor (F a)
H5: forall b : B, Is1Functor (flip F b)
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap01 F a1 g $o fmap10 F f b0 $==
fmap10 F f b1 $o fmap01 F a0 g
Is1Functor (uncurry F) exact _. (* [is1functor_prod_is1functor]. *)
  -
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
H2: forall a : A, Is0Functor (F a)
H3: forall b : B, Is0Functor (flip F b)
Is0Bifunctor_F:= Build_Is0Bifunctor'' F: Is0Bifunctor F
H4: forall a : A, Is1Functor (F a)
H5: forall b : B, Is1Functor (flip F b)
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap01 F a1 g $o fmap10 F f b0 $==
fmap10 F f b1 $o fmap01 F a0 g
forall a : A, Is1Functor (F a) exact _.
  -
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
H2: forall a : A, Is0Functor (F a)
H3: forall b : B, Is0Functor (flip F b)
Is0Bifunctor_F:= Build_Is0Bifunctor'' F: Is0Bifunctor F
H4: forall a : A, Is1Functor (F a)
H5: forall b : B, Is1Functor (flip F b)
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap01 F a1 g $o fmap10 F f b0 $==
fmap10 F f b1 $o fmap01 F a0 g
forall b : B, Is1Functor (flip F b) exact _.
  -
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
H2: forall a : A, Is0Functor (F a)
H3: forall b : B, Is0Functor (flip F b)
Is0Bifunctor_F:= Build_Is0Bifunctor'' F: Is0Bifunctor F
H4: forall a : A, Is1Functor (F a)
H5: forall b : B, Is1Functor (flip F b)
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap01 F a1 g $o fmap10 F f b0 $==
fmap10 F f b1 $o fmap01 F a0 g
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : B) (g : b0 $-> b1),
fmap11 F f g $== fmap01 F a1 g $o fmap10 F f b0 intros a0 a1 f b0 b1 g.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
H2: forall a : A, Is0Functor (F a)
H3: forall b : B, Is0Functor (flip F b)
Is0Bifunctor_F:= Build_Is0Bifunctor'' F: Is0Bifunctor F
H4: forall a : A, Is1Functor (F a)
H5: forall b : B, Is1Functor (flip F b)
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap01 F a1 g $o fmap10 F f b0 $==
fmap10 F f b1 $o fmap01 F a0 g
a0, a1: A
f: a0 $-> a1
b0, b1: B
g: b0 $-> b1
fmap11 F f g $== fmap01 F a1 g $o fmap10 F f b0
    exact (bifunctor_coh a0 a1 f b0 b1 g)^$.
  -
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
H2: forall a : A, Is0Functor (F a)
H3: forall b : B, Is0Functor (flip F b)
Is0Bifunctor_F:= Build_Is0Bifunctor'' F: Is0Bifunctor F
H4: forall a : A, Is1Functor (F a)
H5: forall b : B, Is1Functor (flip F b)
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap01 F a1 g $o fmap10 F f b0 $==
fmap10 F f b1 $o fmap01 F a0 g
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : B) (g : b0 $-> b1),
fmap11 F f g $== fmap10 F f b1 $o fmap01 F a0 g reflexivity.
Defined.

(** ** Bifunctor lemmas *)

(** *** Coherence *)

Definition bifunctor_coh {A B C : Type}
  (F : A -> B -> C) `{Is1Bifunctor A B C F}
  {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)
  : fmap01 F a1 g $o fmap10 F f b0 $== fmap10 F f b1 $o fmap01 F a0 g
  := (fmap11_is_fmap01_fmap10 _ _ _)^$ $@ fmap11_is_fmap10_fmap01 _ _ _.

(** 2-functorial action *)

Definition fmap02 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  (a : A) {b0 b1 : B} {g g' : b0 $-> b1} (q : g $== g')
  : fmap01 F a g $== fmap01 F a g'
  := fmap2 (F a) q.

Definition fmap12 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} {g g' : b0 $-> b1} (q : g $== g')
  : fmap11 F f g $== fmap11 F f g'
  := fmap2_pair (uncurry F) (Id _) q.

Definition fmap20 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  {a0 a1 : A} {f f' : a0 $-> a1} (p : f $== f') (b : B)
  : fmap10 F f b $== fmap10 F f' b
  := fmap2 (flip F b) p.

Definition fmap21 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  {a0 a1 : A} {f f' : a0 $-> a1} (p : f $== f') {b0 b1 : B} (g : b0 $-> b1)
  : fmap11 F f g $== fmap11 F f' g
  := fmap2_pair (uncurry F) p (Id _).

Definition fmap22 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  {a0 a1 : A} {f f' : a0 $-> a1} (p : f $== f')
  {b0 b1 : B} {g g' : b0 $-> b1} (q : g $== g')
  : fmap11 F f g $== fmap11 F f' g'
  := fmap2_pair (uncurry F) p q.

(** *** Identity preservation *)

Definition fmap01_id {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : A) (b : B)
  : fmap01 F a (Id b) $== Id (F a b)
  := fmap_id (F a) b.

Definition fmap10_id {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : A) (b : B)
  : fmap10 F (Id a) b $== Id (F a b)
  := fmap_id (flip F b) a.

Definition fmap11_id {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : A) (b : B)
  : fmap11 F (Id a) (Id b) $== Id (F a b)
  := fmap_id (uncurry F) (a, b).

(** [fmap11] with left map the identity gives [fmap01]. *)
Definition fmap01_is_fmap11 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  (a : A) {b0 b1 : B} (g : b0 $-> b1)
  : fmap11 F (Id a) g $== fmap01 F a g
  := fmap11_is_fmap01_fmap10 _ _ _ $@ (_ $@L fmap10_id _ _ _) $@ cat_idr _.

(** [fmap11] with right map the identity gives [fmap10]. *)
Definition fmap10_is_fmap11 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  {a0 a1 : A} (f : a0 $-> a1) (b : B)
  : fmap11 F f (Id b) $== fmap10 F f b
  := fmap11_is_fmap01_fmap10 _ _ _ $@ (fmap01_id _ _ _ $@R _) $@ cat_idl _.

(** *** Composition preservation *)

Definition fmap01_comp {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  (a : A) {b0 b1 b2 : B} (g : b1 $-> b2) (f : b0 $-> b1)
  : fmap01 F a (g $o f) $== fmap01 F a g $o fmap01 F a f
  := fmap_comp (F a) f g.

Definition fmap10_comp {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  {a0 a1 a2 : A} (g : a1 $-> a2) (f : a0 $-> a1) (b : B)
  : fmap10 F (g $o f) b $== fmap10 F g b $o fmap10 F f b
  := fmap_comp (flip F b) f g.

Definition fmap11_comp {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  {a0 a1 a2 : A} (g : a1 $-> a2) (f : a0 $-> a1)
  {b0 b1 b2 : B} (k : b1 $-> b2) (h : b0 $-> b1)
  : fmap11 F (g $o f) (k $o h) $== fmap11 F g k $o fmap11 F f h
  := fmap_pair_comp (uncurry F) _ _ _ _.

(** *** Equivalence preservation *)

Instance iemap10 {A B C : Type} `{HasEquivs A, Is1Cat B, HasEquivs C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  {a0 a1 : A} (f : a0 $<~> a1) (b : B)
  : CatIsEquiv (fmap10 F f b)
  := iemap (flip F b) f.

Instance iemap01 {A B C : Type} `{Is1Cat A, HasEquivs B, HasEquivs C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  (a : A) {b0 b1 : B} (g : b0 $<~> b1)
  : CatIsEquiv (fmap01 F a g)
  := iemap (F a) g.

Instance iemap11 {A B C : Type} `{HasEquivs A, HasEquivs B, HasEquivs C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  {a0 a1 : A} (f : a0 $<~> a1) {b0 b1 : B} (g : b0 $<~> b1)
  : CatIsEquiv (fmap11 F f g)
  := iemap (uncurry F) (a := (a0, b0)) (b := (_, _)) (f, g).

Definition emap10 {A B C : Type} `{HasEquivs A, Is1Cat B, HasEquivs C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  {a0 a1 : A} (f : a0 $<~> a1) (b : B)
  : F a0 b $<~> F a1 b
  := Build_CatEquiv (fmap10 F f b).

Definition emap01 {A B C : Type} `{Is1Cat A, HasEquivs B, HasEquivs C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  (a : A) {b0 b1 : B} (g : b0 $<~> b1)
  : F a b0 $<~> F a b1
  := Build_CatEquiv (fmap01 F a g).

Definition emap11 {A B C : Type} `{HasEquivs A, HasEquivs B, HasEquivs C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  {a0 a1 : A} (f : a0 $<~> a1) {b0 b1 : B} (g : b0 $<~> b1)
  : F a0 b0 $<~> F a1 b1
  := Build_CatEquiv (fmap11 F f g).

(** ** Flipping bifunctors *)

Definition is0bifunctor_flip {A B C : Type}
  (F : A -> B -> C) `{Is01Cat A, Is01Cat B, Is01Cat C, !Is0Bifunctor F}
  : Is0Bifunctor (flip F).
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
H3: IsGraph C
H4: Is01Cat C
Is0Bifunctor0: Is0Bifunctor F
Is0Bifunctor (flip F)
Proof.
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
H3: IsGraph C
H4: Is01Cat C
Is0Bifunctor0: Is0Bifunctor F
Is0Bifunctor (flip F)
  snapply Build_Is0Bifunctor.
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
H3: IsGraph C
H4: Is01Cat C
Is0Bifunctor0: Is0Bifunctor F
Is0Functor (uncurry (flip F))
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
H3: IsGraph C
H4: Is01Cat C
Is0Bifunctor0: Is0Bifunctor F
forall a : B, Is0Functor (flip F a)
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
H3: IsGraph C
H4: Is01Cat C
Is0Bifunctor0: Is0Bifunctor F
forall b : A, Is0Functor (flip (flip F) b)
  -
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
H3: IsGraph C
H4: Is01Cat C
Is0Bifunctor0: Is0Bifunctor F
Is0Functor (uncurry (flip F)) change (Is0Functor (uncurry F o equiv_prod_symm _ _)).
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
H3: IsGraph C
H4: Is01Cat C
Is0Bifunctor0: Is0Bifunctor F
Is0Functor (uncurry F o equiv_prod_symm B A)
    exact _.
  -
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
H3: IsGraph C
H4: Is01Cat C
Is0Bifunctor0: Is0Bifunctor F
forall a : B, Is0Functor (flip F a) exact _.
  -
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
H3: IsGraph C
H4: Is01Cat C
Is0Bifunctor0: Is0Bifunctor F
forall b : A, Is0Functor (flip (flip F) b) exact _.
Defined.
Hint Immediate is0bifunctor_flip : typeclass_instances.

Definition is1bifunctor_flip {A B C : Type}
(F : A -> B -> C) `{H : Is1Bifunctor A B C F}
  : Is1Bifunctor (flip F).
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H: Is1Bifunctor F
Is1Bifunctor (flip F)
Proof.
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H: Is1Bifunctor F
Is1Bifunctor (flip F)
  snapply Build_Is1Bifunctor.
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H: Is1Bifunctor F
Is1Functor (uncurry (flip F))
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H: Is1Bifunctor F
forall a : B, Is1Functor (flip F a)
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H: Is1Bifunctor F
forall b : A, Is1Functor (flip (flip F) b)
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H: Is1Bifunctor F
forall (a0 a1 : B) (f : a0 $-> a1) 
(b0 b1 : A) (g : b0 $-> b1),
fmap11 (flip F) f g $==
fmap01 (flip F) a1 g $o fmap10 (flip F) f b0
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H: Is1Bifunctor F
forall (a0 a1 : B) (f : a0 $-> a1) 
(b0 b1 : A) (g : b0 $-> b1),
fmap11 (flip F) f g $==
fmap10 (flip F) f b1 $o fmap01 (flip F) a0 g
  -
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H: Is1Bifunctor F
Is1Functor (uncurry (flip F)) change (Is1Functor (uncurry F o equiv_prod_symm _ _)).
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H: Is1Bifunctor F
Is1Functor (uncurry F o equiv_prod_symm B A)
    exact _.
  -
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H: Is1Bifunctor F
forall a : B, Is1Functor (flip F a) exact _.
  -
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H: Is1Bifunctor F
forall b : A, Is1Functor (flip (flip F) b) exact _.
  -
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H: Is1Bifunctor F
forall (a0 a1 : B) (f : a0 $-> a1) 
(b0 b1 : A) (g : b0 $-> b1),
fmap11 (flip F) f g $==
fmap01 (flip F) a1 g $o fmap10 (flip F) f b0 intros b0 b1 g a0 a1 f.
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H: Is1Bifunctor F
b0, b1: B
g: b0 $-> b1
a0, a1: A
f: a0 $-> a1
fmap11 (flip F) g f $==
fmap01 (flip F) b1 f $o fmap10 (flip F) g a0
    exact (fmap11_is_fmap10_fmap01 F f g).
  -
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H: Is1Bifunctor F
forall (a0 a1 : B) (f : a0 $-> a1) 
(b0 b1 : A) (g : b0 $-> b1),
fmap11 (flip F) f g $==
fmap10 (flip F) f b1 $o fmap01 (flip F) a0 g intros b0 b1 g a0 a1 f.
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H: Is1Bifunctor F
b0, b1: B
g: b0 $-> b1
a0, a1: A
f: a0 $-> a1
fmap11 (flip F) g f $==
fmap10 (flip F) g a1 $o fmap01 (flip F) b0 f
    exact (fmap11_is_fmap01_fmap10 F f g).
Defined.
Hint Immediate is1bifunctor_flip : typeclass_instances.

(** ** Composition of bifunctors *)

(** There are 4 different ways to compose a functor with a bifunctor. *)

(** Restricting a functor along a bifunctor yields a bifunctor. *)
Instance is0bifunctor_postcompose {A B C D : Type}
  `{IsGraph A, IsGraph B, IsGraph C, IsGraph D}
  (F : A -> B -> C) {bf : Is0Bifunctor F}
  (G : C -> D) `{!Is0Functor G}
  : Is0Bifunctor (fun a b => G (F a b)) | 10
  := {}.

Instance is1bifunctor_postcompose {A B C D : Type}
  `{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D}
  (F : A -> B -> C) (G : C -> D) `{!Is0Functor G, !Is1Functor G}
  `{!Is0Bifunctor F} {bf : Is1Bifunctor F}
  : Is1Bifunctor (fun a b => G (F a b)) | 10.
A, B, C, D: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
F: A -> B -> C
G: C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
bf: Is1Bifunctor F
Is1Bifunctor (fun (a : A) (b : B) => G (F a b))
Proof.
A, B, C, D: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
F: A -> B -> C
G: C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
bf: Is1Bifunctor F
Is1Bifunctor (fun (a : A) (b : B) => G (F a b))
  snapply Build_Is1Bifunctor.
A, B, C, D: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
F: A -> B -> C
G: C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
bf: Is1Bifunctor F
Is1Functor
  (uncurry (fun (a : A) (b : B) => G (F a b)))
A, B, C, D: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
F: A -> B -> C
G: C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
bf: Is1Bifunctor F
forall a : A,
Is1Functor ((fun (a0 : A) (b : B) => G (F a0 b)) a)
A, B, C, D: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
F: A -> B -> C
G: C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
bf: Is1Bifunctor F
forall b : B,
Is1Functor
  (flip (fun (a : A) (b0 : B) => G (F a b0)) b)
A, B, C, D: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
F: A -> B -> C
G: C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
bf: Is1Bifunctor F
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : B) (g : b0 $-> b1),
fmap11 (fun (a : A) (b : B) => G (F a b)) f g $==
fmap01 (fun (a : A) (b : B) => G (F a b)) a1 g $o
fmap10 (fun (a : A) (b : B) => G (F a b)) f b0
A, B, C, D: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
F: A -> B -> C
G: C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
bf: Is1Bifunctor F
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : B) (g : b0 $-> b1),
fmap11 (fun (a : A) (b : B) => G (F a b)) f g $==
fmap10 (fun (a : A) (b : B) => G (F a b)) f b1 $o
fmap01 (fun (a : A) (b : B) => G (F a b)) a0 g
  1-3: exact _.
A, B, C, D: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
F: A -> B -> C
G: C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
bf: Is1Bifunctor F
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : B) (g : b0 $-> b1),
fmap11 (fun (a : A) (b : B) => G (F a b)) f g $==
fmap01 (fun (a : A) (b : B) => G (F a b)) a1 g $o
fmap10 (fun (a : A) (b : B) => G (F a b)) f b0
A, B, C, D: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
F: A -> B -> C
G: C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
bf: Is1Bifunctor F
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : B) (g : b0 $-> b1),
fmap11 (fun (a : A) (b : B) => G (F a b)) f g $==
fmap10 (fun (a : A) (b : B) => G (F a b)) f b1 $o
fmap01 (fun (a : A) (b : B) => G (F a b)) a0 g
  -
A, B, C, D: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
F: A -> B -> C
G: C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
bf: Is1Bifunctor F
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : B) (g : b0 $-> b1),
fmap11 (fun (a : A) (b : B) => G (F a b)) f g $==
fmap01 (fun (a : A) (b : B) => G (F a b)) a1 g $o
fmap10 (fun (a : A) (b : B) => G (F a b)) f b0 intros a0 a1 f b0 b1 g.
A, B, C, D: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
F: A -> B -> C
G: C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
bf: Is1Bifunctor F
a0, a1: A
f: a0 $-> a1
b0, b1: B
g: b0 $-> b1
fmap11 (fun (a : A) (b : B) => G (F a b)) f g $==
fmap01 (fun (a : A) (b : B) => G (F a b)) a1 g $o
fmap10 (fun (a : A) (b : B) => G (F a b)) f b0
    exact (fmap2 G (fmap11_is_fmap01_fmap10 F f g) $@ fmap_comp G _ _).
  -
A, B, C, D: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
F: A -> B -> C
G: C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
bf: Is1Bifunctor F
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : B) (g : b0 $-> b1),
fmap11 (fun (a : A) (b : B) => G (F a b)) f g $==
fmap10 (fun (a : A) (b : B) => G (F a b)) f b1 $o
fmap01 (fun (a : A) (b : B) => G (F a b)) a0 g intros a0 a1 f b0 b1 g.
A, B, C, D: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
F: A -> B -> C
G: C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
bf: Is1Bifunctor F
a0, a1: A
f: a0 $-> a1
b0, b1: B
g: b0 $-> b1
fmap11 (fun (a : A) (b : B) => G (F a b)) f g $==
fmap10 (fun (a : A) (b : B) => G (F a b)) f b1 $o
fmap01 (fun (a : A) (b : B) => G (F a b)) a0 g
    exact (fmap2 G (fmap11_is_fmap10_fmap01 F f g) $@ fmap_comp G _ _).
Defined.

Instance is0bifunctor_precompose {A B C D E : Type}
  `{IsGraph A, IsGraph B, IsGraph C, IsGraph D, IsGraph E}
  (G : A -> B) (K : E -> C) (F : B -> C -> D)
  `{!Is0Functor G, !Is0Bifunctor F, !Is0Functor K}
  : Is0Bifunctor (fun a b => F (G a) (K b)) | 10.
A, B, C, D, E: Type
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: IsGraph D
H3: IsGraph E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is0Bifunctor0: Is0Bifunctor F
Is0Functor1: Is0Functor K
Is0Bifunctor (fun (a : A) (b : E) => F (G a) (K b))
Proof.
A, B, C, D, E: Type
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: IsGraph D
H3: IsGraph E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is0Bifunctor0: Is0Bifunctor F
Is0Functor1: Is0Functor K
Is0Bifunctor (fun (a : A) (b : E) => F (G a) (K b))
  snapply Build_Is0Bifunctor.
A, B, C, D, E: Type
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: IsGraph D
H3: IsGraph E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is0Bifunctor0: Is0Bifunctor F
Is0Functor1: Is0Functor K
Is0Functor
  (uncurry (fun (a : A) (b : E) => F (G a) (K b)))
A, B, C, D, E: Type
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: IsGraph D
H3: IsGraph E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is0Bifunctor0: Is0Bifunctor F
Is0Functor1: Is0Functor K
forall a : A,
Is0Functor
  ((fun (a0 : A) (b : E) => F (G a0) (K b)) a)
A, B, C, D, E: Type
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: IsGraph D
H3: IsGraph E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is0Bifunctor0: Is0Bifunctor F
Is0Functor1: Is0Functor K
forall b : E,
Is0Functor
  (flip (fun (a : A) (b0 : E) => F (G a) (K b0)) b)
  -
A, B, C, D, E: Type
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: IsGraph D
H3: IsGraph E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is0Bifunctor0: Is0Bifunctor F
Is0Functor1: Is0Functor K
Is0Functor
  (uncurry (fun (a : A) (b : E) => F (G a) (K b))) change (Is0Functor (uncurry F o functor_prod G K)).
A, B, C, D, E: Type
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: IsGraph D
H3: IsGraph E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is0Bifunctor0: Is0Bifunctor F
Is0Functor1: Is0Functor K
Is0Functor (uncurry F o functor_prod G K)
    exact _.
  -
A, B, C, D, E: Type
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: IsGraph D
H3: IsGraph E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is0Bifunctor0: Is0Bifunctor F
Is0Functor1: Is0Functor K
forall a : A,
Is0Functor
  ((fun (a0 : A) (b : E) => F (G a0) (K b)) a) exact _.
  -
A, B, C, D, E: Type
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: IsGraph D
H3: IsGraph E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is0Bifunctor0: Is0Bifunctor F
Is0Functor1: Is0Functor K
forall b : E,
Is0Functor
  (flip (fun (a : A) (b0 : E) => F (G a) (K b0)) b) intros e.
A, B, C, D, E: Type
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: IsGraph D
H3: IsGraph E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is0Bifunctor0: Is0Bifunctor F
Is0Functor1: Is0Functor K
e: E
Is0Functor
  (flip (fun (a : A) (b : E) => F (G a) (K b)) e)
    change (Is0Functor (flip F (K e) o G)).
A, B, C, D, E: Type
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: IsGraph D
H3: IsGraph E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is0Bifunctor0: Is0Bifunctor F
Is0Functor1: Is0Functor K
e: E
Is0Functor (flip F (K e) o G)
    exact _.
Defined.

Instance is1bifunctor_precompose {A B C D E : Type}
  `{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D, Is1Cat E}
  (G : A -> B) (K : E -> C) (F : B -> C -> D)
  `{!Is0Functor G, !Is1Functor G, !Is0Bifunctor F, !Is1Bifunctor F,
    !Is0Functor K, !Is1Functor K}
  : Is1Bifunctor (fun a b => F (G a) (K b)) | 10.
A, B, C, D, E: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Functor1: Is0Functor K
Is1Functor1: Is1Functor K
Is1Bifunctor (fun (a : A) (b : E) => F (G a) (K b))
Proof.
A, B, C, D, E: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Functor1: Is0Functor K
Is1Functor1: Is1Functor K
Is1Bifunctor (fun (a : A) (b : E) => F (G a) (K b))
  snapply Build_Is1Bifunctor.
A, B, C, D, E: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Functor1: Is0Functor K
Is1Functor1: Is1Functor K
Is1Functor
  (uncurry (fun (a : A) (b : E) => F (G a) (K b)))
A, B, C, D, E: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Functor1: Is0Functor K
Is1Functor1: Is1Functor K
forall a : A,
Is1Functor
  ((fun (a0 : A) (b : E) => F (G a0) (K b)) a)
A, B, C, D, E: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Functor1: Is0Functor K
Is1Functor1: Is1Functor K
forall b : E,
Is1Functor
  (flip (fun (a : A) (b0 : E) => F (G a) (K b0)) b)
A, B, C, D, E: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Functor1: Is0Functor K
Is1Functor1: Is1Functor K
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : E) (g : b0 $-> b1),
fmap11 (fun (a : A) (b : E) => F (G a) (K b)) f g $==
fmap01 (fun (a : A) (b : E) => F (G a) (K b)) a1 g $o
fmap10 (fun (a : A) (b : E) => F (G a) (K b)) f b0
A, B, C, D, E: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Functor1: Is0Functor K
Is1Functor1: Is1Functor K
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : E) (g : b0 $-> b1),
fmap11 (fun (a : A) (b : E) => F (G a) (K b)) f g $==
fmap10 (fun (a : A) (b : E) => F (G a) (K b)) f b1 $o
fmap01 (fun (a : A) (b : E) => F (G a) (K b)) a0 g
  -
A, B, C, D, E: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Functor1: Is0Functor K
Is1Functor1: Is1Functor K
Is1Functor
  (uncurry (fun (a : A) (b : E) => F (G a) (K b))) change (Is1Functor (uncurry F o functor_prod G K)).
A, B, C, D, E: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Functor1: Is0Functor K
Is1Functor1: Is1Functor K
Is1Functor (uncurry F o functor_prod G K)
    exact _.
  -
A, B, C, D, E: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Functor1: Is0Functor K
Is1Functor1: Is1Functor K
forall a : A,
Is1Functor
  ((fun (a0 : A) (b : E) => F (G a0) (K b)) a) exact _.
  -
A, B, C, D, E: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Functor1: Is0Functor K
Is1Functor1: Is1Functor K
forall b : E,
Is1Functor
  (flip (fun (a : A) (b0 : E) => F (G a) (K b0)) b) intros e.
A, B, C, D, E: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Functor1: Is0Functor K
Is1Functor1: Is1Functor K
e: E
Is1Functor
  (flip (fun (a : A) (b : E) => F (G a) (K b)) e)
    change (Is1Functor (flip F (K e) o G)).
A, B, C, D, E: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Functor1: Is0Functor K
Is1Functor1: Is1Functor K
e: E
Is1Functor (flip F (K e) o G)
    exact _.
  -
A, B, C, D, E: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Functor1: Is0Functor K
Is1Functor1: Is1Functor K
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : E) (g : b0 $-> b1),
fmap11 (fun (a : A) (b : E) => F (G a) (K b)) f g $==
fmap01 (fun (a : A) (b : E) => F (G a) (K b)) a1 g $o
fmap10 (fun (a : A) (b : E) => F (G a) (K b)) f b0 intros a0 a1 f b0 b1 g.
A, B, C, D, E: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Functor1: Is0Functor K
Is1Functor1: Is1Functor K
a0, a1: A
f: a0 $-> a1
b0, b1: E
g: b0 $-> b1
fmap11 (fun (a : A) (b : E) => F (G a) (K b)) f g $==
fmap01 (fun (a : A) (b : E) => F (G a) (K b)) a1 g $o
fmap10 (fun (a : A) (b : E) => F (G a) (K b)) f b0
    exact (fmap11_is_fmap01_fmap10 F (fmap G f) (fmap K g)).
  -
A, B, C, D, E: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Functor1: Is0Functor K
Is1Functor1: Is1Functor K
forall (a0 a1 : A) (f : a0 $-> a1) 
(b0 b1 : E) (g : b0 $-> b1),
fmap11 (fun (a : A) (b : E) => F (G a) (K b)) f g $==
fmap10 (fun (a : A) (b : E) => F (G a) (K b)) f b1 $o
fmap01 (fun (a : A) (b : E) => F (G a) (K b)) a0 g intros a0 a1 f b0 b1 g.
A, B, C, D, E: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
G: A -> B
K: E -> C
F: B -> C -> D
Is0Functor0: Is0Functor G
Is1Functor0: Is1Functor G
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Functor1: Is0Functor K
Is1Functor1: Is1Functor K
a0, a1: A
f: a0 $-> a1
b0, b1: E
g: b0 $-> b1
fmap11 (fun (a : A) (b : E) => F (G a) (K b)) f g $==
fmap10 (fun (a : A) (b : E) => F (G a) (K b)) f b1 $o
fmap01 (fun (a : A) (b : E) => F (G a) (K b)) a0 g
    exact (fmap11_is_fmap10_fmap01 F (fmap G f) (fmap K g)).
Defined.

Instance is0functor_uncurry_uncurry_left {A B C D E}
  (F : A -> B -> C) (G : C -> D -> E)
  `{IsGraph A, IsGraph B, IsGraph C, IsGraph D, IsGraph E,
    !Is0Bifunctor F, !Is0Bifunctor G}
  : Is0Functor (uncurry (uncurry (fun x y z => G (F x y) z))).
A, B, C, D, E: Type
F: A -> B -> C
G: C -> D -> E
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: IsGraph D
H3: IsGraph E
Is0Bifunctor0: Is0Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
Is0Functor
  (uncurry
     (uncurry
        (fun (x : A) (y : B) (z : D) => G (F x y) z)))
Proof.
A, B, C, D, E: Type
F: A -> B -> C
G: C -> D -> E
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: IsGraph D
H3: IsGraph E
Is0Bifunctor0: Is0Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
Is0Functor
  (uncurry
     (uncurry
        (fun (x : A) (y : B) (z : D) => G (F x y) z)))
  exact _.
Defined.

Instance is1functor_uncurry_uncurry_left {A B C D E}
  (F : A -> B -> C) (G : C -> D -> E)
  `{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D, Is1Cat E,
    !Is0Bifunctor F, !Is1Bifunctor F, !Is0Bifunctor G, !Is1Bifunctor G}
  : Is1Functor (uncurry (uncurry (fun x y z => G (F x y) z))).
A, B, C, D, E: Type
F: A -> B -> C
G: C -> D -> E
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
Is1Functor
  (uncurry
     (uncurry
        (fun (x : A) (y : B) (z : D) => G (F x y) z)))
Proof.
A, B, C, D, E: Type
F: A -> B -> C
G: C -> D -> E
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
Is1Functor
  (uncurry
     (uncurry
        (fun (x : A) (y : B) (z : D) => G (F x y) z)))
  exact _.
Defined.

Instance is0functor_uncurry_uncurry_right {A B C D E}
  (F : A -> B -> D) (G : C -> D -> E)
  `{IsGraph A, IsGraph B, IsGraph C, IsGraph D, IsGraph E,
    !Is0Bifunctor F, !Is0Bifunctor G}
  : Is0Functor (uncurry (uncurry (fun x y z => G x (F y z)))).
A, B, C, D, E: Type
F: A -> B -> D
G: C -> D -> E
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: IsGraph D
H3: IsGraph E
Is0Bifunctor0: Is0Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
Is0Functor
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
Proof.
A, B, C, D, E: Type
F: A -> B -> D
G: C -> D -> E
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: IsGraph D
H3: IsGraph E
Is0Bifunctor0: Is0Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
Is0Functor
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  snapply Build_Is0Functor.
A, B, C, D, E: Type
F: A -> B -> D
G: C -> D -> E
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: IsGraph D
H3: IsGraph E
Is0Bifunctor0: Is0Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
forall a b : C * A * B,
(a $-> b) ->
uncurry
  (uncurry
     (fun (x : C) (y : A) (z : B) => G x (F y z))) a $->
uncurry
  (uncurry
     (fun (x : C) (y : A) (z : B) => G x (F y z))) b
  intros cab cab' [[h f] g].
A, B, C, D, E: Type
F: A -> B -> D
G: C -> D -> E
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: IsGraph D
H3: IsGraph E
Is0Bifunctor0: Is0Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
cab, cab': C * A * B
h: fst (fst cab) $-> fst (fst cab')
f: snd (fst cab) $-> snd (fst cab')
g: snd cab $-> snd cab'
uncurry
  (uncurry
     (fun (x : C) (y : A) (z : B) => G x (F y z))) cab $->
uncurry
  (uncurry
     (fun (x : C) (y : A) (z : B) => G x (F y z)))
  cab'
  exact (fmap11 G h (fmap11 F f g)).
Defined.

Instance is1functor_uncurry_uncurry_right {A B C D E}
  (F : A -> B -> D) (G : C -> D -> E)
  `{Is1Cat A, Is1Cat B, Is1Cat C, Is1Cat D, Is1Cat E,
    !Is0Bifunctor F, !Is1Bifunctor F, !Is0Bifunctor G, !Is1Bifunctor G}
  : Is1Functor (uncurry (uncurry (fun x y z => G x (F y z)))).
A, B, C, D, E: Type
F: A -> B -> D
G: C -> D -> E
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
Is1Functor
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
Proof.
A, B, C, D, E: Type
F: A -> B -> D
G: C -> D -> E
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
Is1Functor
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  snapply Build_Is1Functor.
A, B, C, D, E: Type
F: A -> B -> D
G: C -> D -> E
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
forall (a b : C * A * B) 
(f g : a $-> b),
f $== g ->
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  f $==
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  g
A, B, C, D, E: Type
F: A -> B -> D
G: C -> D -> E
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
forall a : C * A * B,
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  (Id a) $==
Id
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z)))
     a)
A, B, C, D, E: Type
F: A -> B -> D
G: C -> D -> E
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
forall (a b c : C * A * B) 
(f : a $-> b) (g : b $-> c),
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  (g $o f) $==
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  g $o
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  f
  -
A, B, C, D, E: Type
F: A -> B -> D
G: C -> D -> E
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
forall (a b : C * A * B) 
(f g : a $-> b),
f $== g ->
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  f $==
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  g intros cab cab' [[h f] g] [[h' f'] g'] [[q p] r].
A, B, C, D, E: Type
F: A -> B -> D
G: C -> D -> E
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
cab, cab': C * A * B
h: fst (fst cab) $-> fst (fst cab')
f: snd (fst cab) $-> snd (fst cab')
g: snd cab $-> snd cab'
h': fst (fst cab) $-> fst (fst cab')
f': snd (fst cab) $-> snd (fst cab')
g': snd cab $-> snd cab'
q: fst (fst (h, f, g)) $-> fst (fst (h', f', g'))
p: snd (fst (h, f, g)) $-> snd (fst (h', f', g'))
r: snd (h, f, g) $-> snd (h', f', g')
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  (h, f, g) $==
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  (h', f', g')
    exact (fmap22 G q (fmap22 F p r)).
  -
A, B, C, D, E: Type
F: A -> B -> D
G: C -> D -> E
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
forall a : C * A * B,
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  (Id a) $==
Id
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z)))
     a) intros cab.
A, B, C, D, E: Type
F: A -> B -> D
G: C -> D -> E
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
cab: C * A * B
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  (Id cab) $==
Id
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z)))
     cab)
    exact (fmap12 G _ (fmap11_id F _ _) $@ fmap11_id G _ _).
  -
A, B, C, D, E: Type
F: A -> B -> D
G: C -> D -> E
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
forall (a b c : C * A * B) 
(f : a $-> b) (g : b $-> c),
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  (g $o f) $==
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  g $o
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  f intros cab cab' cab'' [[h f] g] [[h' f'] g'].
A, B, C, D, E: Type
F: A -> B -> D
G: C -> D -> E
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H2: Is1Cat D
IsGraph4: IsGraph E
Is2Graph4: Is2Graph E
Is01Cat4: Is01Cat E
H3: Is1Cat E
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
cab, cab', cab'': C * A * B
h: fst (fst cab) $-> fst (fst cab')
f: snd (fst cab) $-> snd (fst cab')
g: snd cab $-> snd cab'
h': fst (fst cab') $-> fst (fst cab'')
f': snd (fst cab') $-> snd (fst cab'')
g': snd cab' $-> snd cab''
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  ((h', f', g') $o (h, f, g)) $==
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  (h', f', g') $o
fmap
  (uncurry
     (uncurry
        (fun (x : C) (y : A) (z : B) => G x (F y z))))
  (h, f, g)
    exact (fmap12 G _ (fmap11_comp F _ _ _ _) $@ fmap11_comp G _ _ _ _).
Defined.  

Definition fmap11_square {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  {a00 a20 a02 a22 : A} {f10 : a00 $-> a20} {f12 : a02 $-> a22}
  {f01 : a00 $-> a02} {f21 : a20 $-> a22}
  {b00 b20 b02 b22 : B} {g10 : b00 $-> b20} {g12 : b02 $-> b22}
  {g01 : b00 $-> b02} {g21 : b20 $-> b22}
  (p : Square f01 f21 f10 f12) (q : Square g01 g21 g10 g12)
  : Square (fmap11 F f01 g01) (fmap11 F f21 g21) (fmap11 F f10 g10) (fmap11 F f12 g12)
  := (fmap11_comp F _ _ _ _)^$ $@ fmap22 F p q $@ fmap11_comp F _ _ _ _.

(** ** Natural transformations between bifunctors *)

(** We can show that an uncurried natural transformation between uncurried bifunctors by composing the naturality square in each variable. *)
Instance is1natural_uncurry {A B C : Type}
  `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
  (G : A -> B -> C) `{!Is0Bifunctor G, !Is1Bifunctor G}
  (alpha : uncurry F $=> uncurry G)
  (nat_l : forall b, Is1Natural (flip F b) (flip G b) (fun x : A => alpha (x, b)))
  (nat_r : forall a, Is1Natural (F a) (G a) (fun y : B => alpha (a, y)))
  : Is1Natural (uncurry F) (uncurry G) alpha.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: uncurry F $=> uncurry G
nat_l: forall b : B,
Is1Natural (flip F b) (flip G b)
  (fun x : A => alpha (x, b))
nat_r: forall a : A,
Is1Natural (F a) (G a)
  (fun y : B => alpha (a, y))
Is1Natural (uncurry F) (uncurry G) alpha
Proof.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: uncurry F $=> uncurry G
nat_l: forall b : B,
Is1Natural (flip F b) (flip G b)
  (fun x : A => alpha (x, b))
nat_r: forall a : A,
Is1Natural (F a) (G a)
  (fun y : B => alpha (a, y))
Is1Natural (uncurry F) (uncurry G) alpha
  snapply Build_Is1Natural.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: uncurry F $=> uncurry G
nat_l: forall b : B,
Is1Natural (flip F b) (flip G b)
  (fun x : A => alpha (x, b))
nat_r: forall a : A,
Is1Natural (F a) (G a)
  (fun y : B => alpha (a, y))
forall (a a' : A * B) (f : a $-> a'),
alpha a' $o fmap (uncurry F) f $==
fmap (uncurry G) f $o alpha a
  intros [a b] [a' b'] [f f']; cbn in *.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: uncurry F $=> uncurry G
nat_l: forall b : B,
Is1Natural (flip F b) (flip G b)
  (fun x : A => alpha (x, b))
nat_r: forall a : A,
Is1Natural (F a) (G a)
  (fun y : B => alpha (a, y))
a: A
b: B
a': A
b': B
f: a $-> a'
f': b $-> b'
alpha (a', b') $o fmap (uncurry F) (f, f') $==
fmap (uncurry G) (f, f') $o alpha (a, b)
  change (?w $o ?x $== ?y $o ?z) with (Square z w x y).
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: uncurry F $=> uncurry G
nat_l: forall b : B,
Is1Natural (flip F b) (flip G b)
  (fun x : A => alpha (x, b))
nat_r: forall a : A,
Is1Natural (F a) (G a)
  (fun y : B => alpha (a, y))
a: A
b: B
a': A
b': B
f: a $-> a'
f': b $-> b'
Square (alpha (a, b)) (alpha (a', b'))
  (fmap (uncurry F) (f, f'))
  (fmap (uncurry G) (f, f'))
  napply vconcatL.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: uncurry F $=> uncurry G
nat_l: forall b : B,
Is1Natural (flip F b) (flip G b)
  (fun x : A => alpha (x, b))
nat_r: forall a : A,
Is1Natural (F a) (G a)
  (fun y : B => alpha (a, y))
a: A
b: B
a': A
b': B
f: a $-> a'
f': b $-> b'
fmap (uncurry F) (f, f') $== ?Goal
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: uncurry F $=> uncurry G
nat_l: forall b : B,
Is1Natural (flip F b) (flip G b)
  (fun x : A => alpha (x, b))
nat_r: forall a : A,
Is1Natural (F a) (G a)
  (fun y : B => alpha (a, y))
a: A
b: B
a': A
b': B
f: a $-> a'
f': b $-> b'
Square (alpha (a, b)) (alpha (a', b')) 
  ?Goal (fmap (uncurry G) (f, f'))
  1: rapply (fmap11_is_fmap01_fmap10 F).
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: uncurry F $=> uncurry G
nat_l: forall b : B,
Is1Natural (flip F b) (flip G b)
  (fun x : A => alpha (x, b))
nat_r: forall a : A,
Is1Natural (F a) (G a)
  (fun y : B => alpha (a, y))
a: A
b: B
a': A
b': B
f: a $-> a'
f': b $-> b'
Square (alpha (a, b)) (alpha (a', b'))
  (fmap01 F (fst (a', b')) f' $o
   fmap10 F f (snd (a, b))) 
  (fmap (uncurry G) (f, f'))
  napply vconcatR.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: uncurry F $=> uncurry G
nat_l: forall b : B,
Is1Natural (flip F b) (flip G b)
  (fun x : A => alpha (x, b))
nat_r: forall a : A,
Is1Natural (F a) (G a)
  (fun y : B => alpha (a, y))
a: A
b: B
a': A
b': B
f: a $-> a'
f': b $-> b'
Square (alpha (a, b)) (alpha (a', b'))
  (fmap01 F (fst (a', b')) f' $o
   fmap10 F f (snd (a, b))) 
  ?Goal
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: uncurry F $=> uncurry G
nat_l: forall b : B,
Is1Natural (flip F b) (flip G b)
  (fun x : A => alpha (x, b))
nat_r: forall a : A,
Is1Natural (F a) (G a)
  (fun y : B => alpha (a, y))
a: A
b: B
a': A
b': B
f: a $-> a'
f': b $-> b'
fmap (uncurry G) (f, f') $== ?Goal
  2: rapply (fmap11_is_fmap01_fmap10 G).
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: uncurry F $=> uncurry G
nat_l: forall b : B,
Is1Natural (flip F b) (flip G b)
  (fun x : A => alpha (x, b))
nat_r: forall a : A,
Is1Natural (F a) (G a)
  (fun y : B => alpha (a, y))
a: A
b: B
a': A
b': B
f: a $-> a'
f': b $-> b'
Square (alpha (a, b)) (alpha (a', b'))
  (fmap01 F (fst (a', b')) f' $o
   fmap10 F f (snd (a, b)))
  (fmap01 G (fst (a', b')) f' $o
   fmap10 G f (snd (a, b)))
  exact (hconcat (nat_l _ _ _ f) (nat_r _ _ _ f')).
Defined.

(** Flipping a natural transformation between bifunctors. *)
Definition nattrans_flip {A B C : Type}
  `{Is1Cat A, Is1Cat B, Is1Cat C}
  {F : A -> B -> C} `{!Is0Bifunctor F, !Is1Bifunctor F}
  {G : A -> B -> C} `{!Is0Bifunctor G, !Is1Bifunctor G}
  : NatTrans (uncurry F) (uncurry G)
    -> NatTrans (uncurry (flip F)) (uncurry (flip G)).
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
NatTrans (uncurry F) (uncurry G) ->
NatTrans (uncurry (flip F)) (uncurry (flip G))
Proof.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
NatTrans (uncurry F) (uncurry G) ->
NatTrans (uncurry (flip F)) (uncurry (flip G))
  intros alpha.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: NatTrans (uncurry F) (uncurry G)
NatTrans (uncurry (flip F)) (uncurry (flip G))
  snapply Build_NatTrans.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: NatTrans (uncurry F) (uncurry G)
uncurry (flip F) $=> uncurry (flip G)
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: NatTrans (uncurry F) (uncurry G)
Is1Natural (uncurry (flip F)) 
  (uncurry (flip G)) ?alpha
  -
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: NatTrans (uncurry F) (uncurry G)
uncurry (flip F) $=> uncurry (flip G) exact (alpha o equiv_prod_symm _ _).
  -
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: NatTrans (uncurry F) (uncurry G)
Is1Natural (uncurry (flip F)) 
  (uncurry (flip G)) (alpha o equiv_prod_symm B A) snapply Build_Is1Natural'.
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: NatTrans (uncurry F) (uncurry G)
forall (a a' : B * A) (f : a $-> a'),
(fun x : B * A => alpha (equiv_prod_symm B A x)) a' $o
fmap (uncurry (flip F)) f $==
fmap (uncurry (flip G)) f $o
(fun x : B * A => alpha (equiv_prod_symm B A x)) a
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: NatTrans (uncurry F) (uncurry G)
forall (a a' : B * A) (f : a $-> a'),
fmap (uncurry (flip G)) f $o
(fun x : B * A => alpha (equiv_prod_symm B A x)) a $==
(fun x : B * A => alpha (equiv_prod_symm B A x)) a' $o
fmap (uncurry (flip F)) f
    +
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: NatTrans (uncurry F) (uncurry G)
forall (a a' : B * A) (f : a $-> a'),
(fun x : B * A => alpha (equiv_prod_symm B A x)) a' $o
fmap (uncurry (flip F)) f $==
fmap (uncurry (flip G)) f $o
(fun x : B * A => alpha (equiv_prod_symm B A x)) a intros [b a] [b' a'] [g f].
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: NatTrans (uncurry F) (uncurry G)
b: B
a: A
b': B
a': A
g: fst (b, a) $-> fst (b', a')
f: snd (b, a) $-> snd (b', a')
alpha (equiv_prod_symm B A (b', a')) $o
fmap (uncurry (flip F)) (g, f) $==
fmap (uncurry (flip G)) (g, f) $o
alpha (equiv_prod_symm B A (b, a))
      exact (isnat (a:=(a, b)) (a':=(a', b')) alpha (f, g)).
    +
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: NatTrans (uncurry F) (uncurry G)
forall (a a' : B * A) (f : a $-> a'),
fmap (uncurry (flip G)) f $o
(fun x : B * A => alpha (equiv_prod_symm B A x)) a $==
(fun x : B * A => alpha (equiv_prod_symm B A x)) a' $o
fmap (uncurry (flip F)) f intros [b a] [b' a'] [g f].
A, B, C: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
F: A -> B -> C
Is0Bifunctor0: Is0Bifunctor F
Is1Bifunctor0: Is1Bifunctor F
G: A -> B -> C
Is0Bifunctor1: Is0Bifunctor G
Is1Bifunctor1: Is1Bifunctor G
alpha: NatTrans (uncurry F) (uncurry G)
b: B
a: A
b': B
a': A
g: fst (b, a) $-> fst (b', a')
f: snd (b, a) $-> snd (b', a')
fmap (uncurry (flip G)) (g, f) $o
alpha (equiv_prod_symm B A (b, a)) $==
alpha (equiv_prod_symm B A (b', a')) $o
fmap (uncurry (flip F)) (g, f)
      exact (isnat_tr (a:=(a, b)) (a':=(a', b')) alpha (f, g)).
Defined.

(** ** Opposite Bifunctors *)

(** There are a few more combinations we can do for this, such as profunctors, but we will leave those for later. *)

Instance is0bifunctor_op A B C (F : A -> B -> C) `{Is0Bifunctor A B C F}
  : Is0Bifunctor (F : A^op -> B^op -> C^op).
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: Is0Bifunctor F
Is0Bifunctor (F : A^op -> B^op -> C^op)
Proof.
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: Is0Bifunctor F
Is0Bifunctor (F : A^op -> B^op -> C^op)
  snapply Build_Is0Bifunctor.
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: Is0Bifunctor F
Is0Functor (uncurry F)
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: Is0Bifunctor F
forall a : A^op, Is0Functor (F a)
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: Is0Bifunctor F
forall b : B^op, Is0Functor (flip F b)
  -
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: Is0Bifunctor F
Is0Functor (uncurry F) exact (is0functor_op _ _ (uncurry F)).
  -
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: Is0Bifunctor F
forall a : A^op, Is0Functor (F a) intros a.
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: Is0Bifunctor F
a: A^op
Is0Functor (F a)
    napply is0functor_op.
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: Is0Bifunctor F
a: A^op
Is0Functor (F a)
    exact (is0functor01_bifunctor F a).
  -
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: Is0Bifunctor F
forall b : B^op, Is0Functor (flip F b) intros b.
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: Is0Bifunctor F
b: B^op
Is0Functor (flip F b)
    napply is0functor_op.
A, B, C: Type
F: A -> B -> C
H: IsGraph A
H0: IsGraph B
H1: IsGraph C
H2: Is0Bifunctor F
b: B^op
Is0Functor (flip F b)
    exact (is0functor10_bifunctor F b).
Defined.

Instance is1bifunctor_op A B C (F : A -> B -> C) `{Is1Bifunctor A B C F}
  : Is1Bifunctor (F : A^op -> B^op -> C^op).
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
Is1Bifunctor (F : A^op -> B^op -> C^op)
Proof.
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
Is1Bifunctor (F : A^op -> B^op -> C^op)
  snapply Build_Is1Bifunctor.
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
Is1Functor (uncurry F)
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
forall a : A^op, Is1Functor (F a)
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
forall b : B^op, Is1Functor (flip F b)
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
forall (a0 a1 : A^op) (f : a0 $-> a1) 
(b0 b1 : B^op) (g : b0 $-> b1),
fmap11 F f g $== fmap01 F a1 g $o fmap10 F f b0
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
forall (a0 a1 : A^op) (f : a0 $-> a1) 
(b0 b1 : B^op) (g : b0 $-> b1),
fmap11 F f g $== fmap10 F f b1 $o fmap01 F a0 g
  -
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
Is1Functor (uncurry F) exact (is1functor_op _ _ (uncurry F)).
  -
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
forall a : A^op, Is1Functor (F a) intros a.
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
a: A^op
Is1Functor (F a)
    napply is1functor_op.
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
a: A^op
Is1Functor (F a)
    exact (is1functor01_bifunctor F a).
  -
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
forall b : B^op, Is1Functor (flip F b) intros b.
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
b: B^op
Is1Functor (flip F b)
    napply is1functor_op.
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
b: B^op
Is1Functor (flip F b)
    exact (is1functor10_bifunctor F b).
  -
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
forall (a0 a1 : A^op) (f : a0 $-> a1) 
(b0 b1 : B^op) (g : b0 $-> b1),
fmap11 F f g $== fmap01 F a1 g $o fmap10 F f b0 intros a0 a1 f b0 b1 g; cbn in f, g.
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
a0, a1: A^op
f: a1 $-> a0
b0, b1: B^op
g: b1 $-> b0
fmap11 F f g $== fmap01 F a1 g $o fmap10 F f b0
    exact (fmap11_is_fmap10_fmap01 F f g).
  -
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
forall (a0 a1 : A^op) (f : a0 $-> a1) 
(b0 b1 : B^op) (g : b0 $-> b1),
fmap11 F f g $== fmap10 F f b1 $o fmap01 F a0 g intros a0 a1 f b0 b1 g; cbn in f, g.
A, B, C: Type
F: A -> B -> C
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H1: Is1Cat C
Is0Bifunctor0: Is0Bifunctor F
H2: Is1Bifunctor F
a0, a1: A^op
f: a1 $-> a0
b0, b1: B^op
g: b1 $-> b0
fmap11 F f g $== fmap10 F f b1 $o fmap01 F a0 g
    exact (fmap11_is_fmap01_fmap10 F f g).
Defined.

Instance is0bifunctor_op' A B C (F : A^op -> B^op -> C^op)
  `{IsGraph A, IsGraph B, IsGraph C, Fop : !Is0Bifunctor (F : A^op -> B^op -> C^op)}
  : Is0Bifunctor (F : A -> B -> C)
  := is0bifunctor_op A^op B^op C^op F.

Instance is1bifunctor_op' A B C (F : A^op -> B^op -> C^op)
  `{Is1Cat A, Is1Cat B, Is1Cat C,
    !Is0Bifunctor (F : A^op -> B^op -> C^op), !Is1Bifunctor (F : A^op -> B^op -> C^op)}
  : Is1Bifunctor (F : A -> B -> C)
  := is1bifunctor_op A^op B^op C^op F.