Bifunctor.v

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.

(** * 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);
}.

(** 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
  snrapply 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]. *)
  rapply Build_Is0Bifunctor.
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 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
  snrapply 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
  snrapply 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 *)

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

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

Global 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)
  snrapply 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)
  snrapply 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. *)
Global 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))
  := {}.

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

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

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

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

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

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. *)
Global 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
  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'))
  nrapply 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'))
  nrapply 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.