(* -*- mode: coq; mode: visual-line -*-  *)

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

(** * Product categories *)

(** Products preserve (0,1)-categories. *)
Global Instance isgraph_prod A B `{IsGraph A} `{IsGraph B}
  : IsGraph (A * B)
  := Build_IsGraph (A * B) (fun x y => (fst x $-> fst y) * (snd x $-> snd y)).

Global Instance is01cat_prod A B `{Is01Cat A} `{Is01Cat B}
  : Is01Cat (A * B).
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
Is01Cat (A * B)
Proof.
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
Is01Cat (A * B)
  econstructor.
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
forall a : A * B, a $-> a
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
forall a b c : A * B,
(b $-> c) -> (a $-> b) -> a $-> c
  -
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
forall a : A * B, a $-> a intros [a b]; exact (Id a, Id b).
  -
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
forall a b c : A * B,
(b $-> c) -> (a $-> b) -> a $-> c intros [a1 b1] [a2 b2] [a3 b3] [f1 g1] [f2 g2]; cbn in *.
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
H2: Is01Cat B
a1: A
b1: B
a2: A
b2: B
a3: A
b3: B
f1: a2 $-> a3
g1: b2 $-> b3
f2: a1 $-> a2
g2: b1 $-> b2
(a1 $-> a3) * (b1 $-> b3)
    exact (f1 $o f2 , g1 $o g2).
Defined.

Global Instance is0gpd_prod A B `{Is0Gpd A} `{Is0Gpd B}
 : Is0Gpd (A * B).
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Gpd (A * B)
Proof.
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
Is0Gpd (A * B)
  srapply Build_Is0Gpd.
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
forall a b : A * B, (a $-> b) -> b $-> a
  intros [x1 x2] [y1 y2] [f1 f2].
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
x1: A
x2: B
y1: A
y2: B
f1: fst (x1, x2) $-> fst (y1, y2)
f2: snd (x1, x2) $-> snd (y1, y2)
(y1, y2) $-> (x1, x2)
  cbn in *.
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: Is0Gpd A
H2: IsGraph B
H3: Is01Cat B
H4: Is0Gpd B
x1: A
x2: B
y1: A
y2: B
f1: x1 $-> y1
f2: x2 $-> y2
(y1 $-> x1) * (y2 $-> x2)
  exact ( (f1^$, f2^$) ).
Defined.

Global Instance is2graph_prod A B `{Is2Graph A, Is2Graph B}
  : Is2Graph (A * B).
A, B: Type
H: IsGraph A
H0: Is2Graph A
H1: IsGraph B
H2: Is2Graph B
Is2Graph (A * B)
Proof.
A, B: Type
H: IsGraph A
H0: Is2Graph A
H1: IsGraph B
H2: Is2Graph B
Is2Graph (A * B)
  intros [x1 x2] [y1 y2].
A, B: Type
H: IsGraph A
H0: Is2Graph A
H1: IsGraph B
H2: Is2Graph B
x1: A
x2: B
y1: A
y2: B
IsGraph ((x1, x2) $-> (y1, y2))
  rapply isgraph_prod.
Defined.

Global Instance is1cat_prod A B `{Is1Cat A} `{Is1Cat B}
  : Is1Cat (A * B).
A, B: 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
Is1Cat (A * B)
Proof.
A, B: 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
Is1Cat (A * B)
  srapply Build_Is1Cat.
A, B: 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
forall (a b c : A * B) 
(g : b $-> c), Is0Functor (cat_postcomp a g)
A, B: 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
forall (a b c : A * B) 
(f : a $-> b), Is0Functor (cat_precomp c f)
A, B: 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
forall (a b c d : A * B) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o g $o f $== h $o (g $o f)
A, B: 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
forall (a b c d : A * B) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o (g $o f) $== h $o g $o f
A, B: 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
forall (a b : A * B) (f : a $-> b), Id b $o f $== f
A, B: 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
forall (a b : A * B) (f : a $-> b), f $o Id a $== f
  -
A, B: 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
forall (a b c : A * B) 
(g : b $-> c), Is0Functor (cat_postcomp a g) intros [x1 x2] [y1 y2] [z1 z2] [h1 h2].
A, B: 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
x1: A
x2: B
y1: A
y2: B
z1: A
z2: B
h1: fst (y1, y2) $-> fst (z1, z2)
h2: snd (y1, y2) $-> snd (z1, z2)
Is0Functor (cat_postcomp (x1, x2) (h1, h2))
    srapply Build_Is0Functor.
A, B: 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
x1: A
x2: B
y1: A
y2: B
z1: A
z2: B
h1: fst (y1, y2) $-> fst (z1, z2)
h2: snd (y1, y2) $-> snd (z1, z2)
forall a b : (x1, x2) $-> (y1, y2),
(a $-> b) ->
cat_postcomp (x1, x2) (h1, h2) a $->
cat_postcomp (x1, x2) (h1, h2) b
    intros [f1 f2] [g1 g2] [p1 p2]; cbn in *.
A, B: 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
x1: A
x2: B
y1: A
y2: B
z1: A
z2: B
h1: y1 $-> z1
h2: y2 $-> z2
f1: x1 $-> y1
f2: x2 $-> y2
g1: x1 $-> y1
g2: x2 $-> y2
p1: f1 $-> g1
p2: f2 $-> g2
(h1 $o f1 $-> h1 $o g1) * (h2 $o f2 $-> h2 $o g2)
    exact ( h1 $@L p1 , h2 $@L p2 ).
  -
A, B: 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
forall (a b c : A * B) 
(f : a $-> b), Is0Functor (cat_precomp c f) intros [x1 x2] [y1 y2] [z1 z2] [h1 h2].
A, B: 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
x1: A
x2: B
y1: A
y2: B
z1: A
z2: B
h1: fst (x1, x2) $-> fst (y1, y2)
h2: snd (x1, x2) $-> snd (y1, y2)
Is0Functor (cat_precomp (z1, z2) (h1, h2))
    srapply Build_Is0Functor.
A, B: 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
x1: A
x2: B
y1: A
y2: B
z1: A
z2: B
h1: fst (x1, x2) $-> fst (y1, y2)
h2: snd (x1, x2) $-> snd (y1, y2)
forall a b : (y1, y2) $-> (z1, z2),
(a $-> b) ->
cat_precomp (z1, z2) (h1, h2) a $->
cat_precomp (z1, z2) (h1, h2) b
    intros [f1 f2] [g1 g2] [p1 p2]; cbn in *.
A, B: 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
x1: A
x2: B
y1: A
y2: B
z1: A
z2: B
h1: x1 $-> y1
h2: x2 $-> y2
f1: y1 $-> z1
f2: y2 $-> z2
g1: y1 $-> z1
g2: y2 $-> z2
p1: f1 $-> g1
p2: f2 $-> g2
(f1 $o h1 $-> g1 $o h1) * (f2 $o h2 $-> g2 $o h2)
    exact ( p1 $@R h1 , p2 $@R h2 ).
  -
A, B: 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
forall (a b c d : A * B) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o g $o f $== h $o (g $o f) intros [a1 a2] [b1 b2] [c1 c2] [d1 d2] [f1 f2] [g1 g2] [h1 h2].
A, B: 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
a1: A
a2: B
b1: A
b2: B
c1: A
c2: B
d1: A
d2: B
f1: fst (a1, a2) $-> fst (b1, b2)
f2: snd (a1, a2) $-> snd (b1, b2)
g1: fst (b1, b2) $-> fst (c1, c2)
g2: snd (b1, b2) $-> snd (c1, c2)
h1: fst (c1, c2) $-> fst (d1, d2)
h2: snd (c1, c2) $-> snd (d1, d2)
(h1, h2) $o (g1, g2) $o (f1, f2) $==
(h1, h2) $o ((g1, g2) $o (f1, f2))
    cbn in *.
A, B: 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
a1: A
a2: B
b1: A
b2: B
c1: A
c2: B
d1: A
d2: B
f1: a1 $-> b1
f2: a2 $-> b2
g1: b1 $-> c1
g2: b2 $-> c2
h1: c1 $-> d1
h2: c2 $-> d2
(h1 $o g1 $o f1 $-> h1 $o (g1 $o f1)) *
(h2 $o g2 $o f2 $-> h2 $o (g2 $o f2))
    exact(cat_assoc f1 g1 h1, cat_assoc f2 g2 h2).
  -
A, B: 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
forall (a b c d : A * B) 
(f : a $-> b) (g : b $-> c) 
(h : c $-> d), h $o (g $o f) $== h $o g $o f intros [a1 a2] [b1 b2] [c1 c2] [d1 d2] [f1 f2] [g1 g2] [h1 h2].
A, B: 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
a1: A
a2: B
b1: A
b2: B
c1: A
c2: B
d1: A
d2: B
f1: fst (a1, a2) $-> fst (b1, b2)
f2: snd (a1, a2) $-> snd (b1, b2)
g1: fst (b1, b2) $-> fst (c1, c2)
g2: snd (b1, b2) $-> snd (c1, c2)
h1: fst (c1, c2) $-> fst (d1, d2)
h2: snd (c1, c2) $-> snd (d1, d2)
(h1, h2) $o ((g1, g2) $o (f1, f2)) $==
(h1, h2) $o (g1, g2) $o (f1, f2)
    cbn in *.
A, B: 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
a1: A
a2: B
b1: A
b2: B
c1: A
c2: B
d1: A
d2: B
f1: a1 $-> b1
f2: a2 $-> b2
g1: b1 $-> c1
g2: b2 $-> c2
h1: c1 $-> d1
h2: c2 $-> d2
(h1 $o (g1 $o f1) $-> h1 $o g1 $o f1) *
(h2 $o (g2 $o f2) $-> h2 $o g2 $o f2)
    exact(cat_assoc_opp f1 g1 h1, cat_assoc_opp f2 g2 h2).
  -
A, B: 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
forall (a b : A * B) (f : a $-> b), Id b $o f $== f intros [a1 a2] [b1 b2] [f1 f2].
A, B: 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
a1: A
a2: B
b1: A
b2: B
f1: fst (a1, a2) $-> fst (b1, b2)
f2: snd (a1, a2) $-> snd (b1, b2)
Id (b1, b2) $o (f1, f2) $== (f1, f2)
    cbn in *.
A, B: 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
a1: A
a2: B
b1: A
b2: B
f1: a1 $-> b1
f2: a2 $-> b2
(Id b1 $o f1 $-> f1) * (Id b2 $o f2 $-> f2)
    exact (cat_idl _, cat_idl _).
  -
A, B: 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
forall (a b : A * B) (f : a $-> b), f $o Id a $== f intros [a1 a2] [b1 b2] [g1 g2].
A, B: 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
a1: A
a2: B
b1: A
b2: B
g1: fst (a1, a2) $-> fst (b1, b2)
g2: snd (a1, a2) $-> snd (b1, b2)
(g1, g2) $o Id (a1, a2) $== (g1, g2)
    cbn in *.
A, B: 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
a1: A
a2: B
b1: A
b2: B
g1: a1 $-> b1
g2: a2 $-> b2
(g1 $o Id a1 $-> g1) * (g2 $o Id a2 $-> g2)
    exact (cat_idr _, cat_idr _).
Defined.

(** Product categories inherit equivalences *)

Global Instance hasequivs_prod A B `{HasEquivs A} `{HasEquivs B}
  : HasEquivs (A * B).
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
HasEquivs (A * B)
Proof.
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
HasEquivs (A * B)
  srefine (Build_HasEquivs (A * B) _ _ _ _
             (fun a b => (fst a $<~> fst b) * (snd a $<~> snd b))
             _ _ _ _ _ _ _ _ _).
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall a b : A * B, (a $-> b) -> Type
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall a b : A * B,
(fun a0 b0 : A * B =>
 (fst a0 $<~> fst b0) * (snd a0 $<~> snd b0)) a b ->
a $-> b
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : A * B)
(f : (fun a0 b0 : A * B =>
      (fst a0 $<~> fst b0) * (snd a0 $<~> snd b0)) a b),
?CatIsEquiv' a b (?cate_fun' a b f)
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : A * B) (f : a $-> b),
?CatIsEquiv' a b f ->
(fun a0 b0 : A * B =>
 (fst a0 $<~> fst b0) * (snd a0 $<~> snd b0)) a b
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : A * B) (f : a $-> b)
(fe : ?CatIsEquiv' a b f),
?cate_fun' a b (?cate_buildequiv' a b f fe) $== f
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall a b : A * B,
(fun a0 b0 : A * B =>
 (fst a0 $<~> fst b0) * (snd a0 $<~> snd b0)) a b ->
b $-> a
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : A * B)
(f : (fun a0 b0 : A * B =>
      (fst a0 $<~> fst b0) * (snd a0 $<~> snd b0)) a b),
?cate_inv' a b f $o ?cate_fun' a b f $== Id a
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : A * B)
(f : (fun a0 b0 : A * B =>
      (fst a0 $<~> fst b0) * (snd a0 $<~> snd b0)) a b),
?cate_fun' a b f $o ?cate_inv' a b f $== Id b
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : A * B) (f : a $-> b) 
(g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a -> ?CatIsEquiv' a b f
  1:intros a b f; exact (CatIsEquiv (fst f) * CatIsEquiv (snd f)).
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall a b : A * B,
(fun a0 b0 : A * B =>
 (fst a0 $<~> fst b0) * (snd a0 $<~> snd b0)) a b ->
a $-> b
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : A * B)
(f : (fun a0 b0 : A * B =>
      (fst a0 $<~> fst b0) * (snd a0 $<~> snd b0)) a b),
(fun (a0 b0 : A * B) (f0 : a0 $-> b0) =>
 CatIsEquiv (fst f0) * CatIsEquiv (snd f0)) a b
  (?cate_fun' a b f)
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : A * B) (f : a $-> b),
(fun (a0 b0 : A * B) (f0 : a0 $-> b0) =>
 CatIsEquiv (fst f0) * CatIsEquiv (snd f0)) a b f ->
(fun a0 b0 : A * B =>
 (fst a0 $<~> fst b0) * (snd a0 $<~> snd b0)) a b
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : A * B) (f : a $-> b)
(fe : (fun (a0 b0 : A * B) (f0 : a0 $-> b0) =>
       CatIsEquiv (fst f0) * CatIsEquiv (snd f0)) a b
        f),
?cate_fun' a b (?cate_buildequiv' a b f fe) $== f
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall a b : A * B,
(fun a0 b0 : A * B =>
 (fst a0 $<~> fst b0) * (snd a0 $<~> snd b0)) a b ->
b $-> a
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : A * B)
(f : (fun a0 b0 : A * B =>
      (fst a0 $<~> fst b0) * (snd a0 $<~> snd b0)) a b),
?cate_inv' a b f $o ?cate_fun' a b f $== Id a
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : A * B)
(f : (fun a0 b0 : A * B =>
      (fst a0 $<~> fst b0) * (snd a0 $<~> snd b0)) a b),
?cate_fun' a b f $o ?cate_inv' a b f $== Id b
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
forall (a b : A * B) (f : a $-> b) 
(g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a ->
(fun (a0 b0 : A * B) (f0 : a0 $-> b0) =>
 CatIsEquiv (fst f0) * CatIsEquiv (snd f0)) a b f
  all:cbn; intros a b f.
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $<~> fst b) * (snd a $<~> snd b)
(fst a $-> fst b) * (snd a $-> snd b)
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $<~> fst b) * (snd a $<~> snd b)
CatIsEquiv
  (fst
     ((fun (a b : A * B)
         (f : (fst a $<~> fst b) * (snd a $<~> snd b))
       => ?Goal) a b f)) *
CatIsEquiv
  (snd
     ((fun (a b : A * B)
         (f : (fst a $<~> fst b) * (snd a $<~> snd b))
       => ?Goal) a b f))
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $-> fst b) * (snd a $-> snd b)
CatIsEquiv (fst f) * CatIsEquiv (snd f) ->
(fst a $<~> fst b) * (snd a $<~> snd b)
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $-> fst b) * (snd a $-> snd b)
forall fe : CatIsEquiv (fst f) * CatIsEquiv (snd f),
(fst
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => ?Goal) a b
      ((fun (a b : A * B)
          (f : (fst a $-> fst b) * (snd a $-> snd b))
        => ?Goal1) a b f fe)) $-> 
 fst f) *
(snd
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => ?Goal) a b
      ((fun (a b : A * B)
          (f : (fst a $-> fst b) * (snd a $-> snd b))
        => ?Goal1) a b f fe)) $-> 
 snd f)
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $<~> fst b) * (snd a $<~> snd b)
(fst b $-> fst a) * (snd b $-> snd a)
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $<~> fst b) * (snd a $<~> snd b)
(fst
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => ?Goal3) a b f) $o
 fst
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => ?Goal) a b f) $-> 
 Id (fst a)) *
(snd
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => ?Goal3) a b f) $o
 snd
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => ?Goal) a b f) $-> 
 Id (snd a))
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $<~> fst b) * (snd a $<~> snd b)
(fst
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => ?Goal) a b f) $o
 fst
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => ?Goal3) a b f) $-> 
 Id (fst b)) *
(snd
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => ?Goal) a b f) $o
 snd
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => ?Goal3) a b f) $-> 
 Id (snd b))
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $-> fst b) * (snd a $-> snd b)
forall g : (fst b $-> fst a) * (snd b $-> snd a),
(fst f $o fst g $-> Id (fst b)) *
(snd f $o snd g $-> Id (snd b)) ->
(fst g $o fst f $-> Id (fst a)) *
(snd g $o snd f $-> Id (snd a)) ->
CatIsEquiv (fst f) * CatIsEquiv (snd f)
  -
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $<~> fst b) * (snd a $<~> snd b)
(fst a $-> fst b) * (snd a $-> snd b) split; [ exact (fst f) | exact (snd f) ].
  -
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $<~> fst b) * (snd a $<~> snd b)
CatIsEquiv
  (fst
     ((fun (a b : A * B)
         (f : (fst a $<~> fst b) * (snd a $<~> snd b))
       => (fst f, snd f)) a b f)) *
CatIsEquiv
  (snd
     ((fun (a b : A * B)
         (f : (fst a $<~> fst b) * (snd a $<~> snd b))
       => (fst f, snd f)) a b f)) split; exact _.
  -
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $-> fst b) * (snd a $-> snd b)
CatIsEquiv (fst f) * CatIsEquiv (snd f) ->
(fst a $<~> fst b) * (snd a $<~> snd b) intros [fe1 fe2]; split.
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $-> fst b) * (snd a $-> snd b)
fe1: CatIsEquiv (fst f)
fe2: CatIsEquiv (snd f)
fst a $<~> fst b
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $-> fst b) * (snd a $-> snd b)
fe1: CatIsEquiv (fst f)
fe2: CatIsEquiv (snd f)
snd a $<~> snd b
    +
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $-> fst b) * (snd a $-> snd b)
fe1: CatIsEquiv (fst f)
fe2: CatIsEquiv (snd f)
fst a $<~> fst b exact (Build_CatEquiv (fst f)).
    +
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $-> fst b) * (snd a $-> snd b)
fe1: CatIsEquiv (fst f)
fe2: CatIsEquiv (snd f)
snd a $<~> snd b exact (Build_CatEquiv (snd f)).
  -
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $-> fst b) * (snd a $-> snd b)
forall fe : CatIsEquiv (fst f) * CatIsEquiv (snd f),
(fst
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => (fst f, snd f)) a b
      ((fun (a b : A * B)
          (f : (fst a $-> fst b) * (snd a $-> snd b))
          (X : CatIsEquiv (fst f) * CatIsEquiv (snd f))
        =>
        (fun (fe1 : CatIsEquiv (fst f))
           (fe2 : CatIsEquiv (snd f)) =>
         (Build_CatEquiv (fst f),
         Build_CatEquiv (snd f))) 
          (fst X) (snd X)) a b f fe)) $-> 
 fst f) *
(snd
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => (fst f, snd f)) a b
      ((fun (a b : A * B)
          (f : (fst a $-> fst b) * (snd a $-> snd b))
          (X : CatIsEquiv (fst f) * CatIsEquiv (snd f))
        =>
        (fun (fe1 : CatIsEquiv (fst f))
           (fe2 : CatIsEquiv (snd f)) =>
         (Build_CatEquiv (fst f),
         Build_CatEquiv (snd f))) 
          (fst X) (snd X)) a b f fe)) $-> 
 snd f) intros [fe1 fe2]; cbn; split; apply cate_buildequiv_fun.
  -
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $<~> fst b) * (snd a $<~> snd b)
(fst b $-> fst a) * (snd b $-> snd a) split; [ exact ((fst f)^-1$) | exact ((snd f)^-1$) ].
  -
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $<~> fst b) * (snd a $<~> snd b)
(fst
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => ((fst f)^-1$, (snd f)^-1$)) a b f) $o
 fst
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => (fst f, snd f)) a b f) $-> 
 Id (fst a)) *
(snd
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => ((fst f)^-1$, (snd f)^-1$)) a b f) $o
 snd
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => (fst f, snd f)) a b f) $-> 
 Id (snd a)) split; apply cate_issect.
  -
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $<~> fst b) * (snd a $<~> snd b)
(fst
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => (fst f, snd f)) a b f) $o
 fst
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => ((fst f)^-1$, (snd f)^-1$)) a b f) $->
 Id (fst b)) *
(snd
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => (fst f, snd f)) a b f) $o
 snd
   ((fun (a b : A * B)
       (f : (fst a $<~> fst b) * (snd a $<~> snd b))
     => ((fst f)^-1$, (snd f)^-1$)) a b f) $->
 Id (snd b)) split; apply cate_isretr.
  -
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $-> fst b) * (snd a $-> snd b)
forall g : (fst b $-> fst a) * (snd b $-> snd a),
(fst f $o fst g $-> Id (fst b)) *
(snd f $o snd g $-> Id (snd b)) ->
(fst g $o fst f $-> Id (fst a)) *
(snd g $o snd f $-> Id (snd a)) ->
CatIsEquiv (fst f) * CatIsEquiv (snd f) intros g r s; split.
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $-> fst b) * (snd a $-> snd b)
g: (fst b $-> fst a) * (snd b $-> snd a)
r: (fst f $o fst g $-> Id (fst b)) *
(snd f $o snd g $-> Id (snd b))
s: (fst g $o fst f $-> Id (fst a)) *
(snd g $o snd f $-> Id (snd a))
CatIsEquiv (fst f)
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $-> fst b) * (snd a $-> snd b)
g: (fst b $-> fst a) * (snd b $-> snd a)
r: (fst f $o fst g $-> Id (fst b)) *
(snd f $o snd g $-> Id (snd b))
s: (fst g $o fst f $-> Id (fst a)) *
(snd g $o snd f $-> Id (snd a))
CatIsEquiv (snd f)
    +
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $-> fst b) * (snd a $-> snd b)
g: (fst b $-> fst a) * (snd b $-> snd a)
r: (fst f $o fst g $-> Id (fst b)) *
(snd f $o snd g $-> Id (snd b))
s: (fst g $o fst f $-> Id (fst a)) *
(snd g $o snd f $-> Id (snd a))
CatIsEquiv (fst f) exact (catie_adjointify (fst f) (fst g) (fst r) (fst s)).
    +
A, B: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H1: Is1Cat B
H2: HasEquivs B
a, b: A * B
f: (fst a $-> fst b) * (snd a $-> snd b)
g: (fst b $-> fst a) * (snd b $-> snd a)
r: (fst f $o fst g $-> Id (fst b)) *
(snd f $o snd g $-> Id (snd b))
s: (fst g $o fst f $-> Id (fst a)) *
(snd g $o snd f $-> Id (snd a))
CatIsEquiv (snd f) exact (catie_adjointify (snd f) (snd g) (snd r) (snd s)).
Defined.

Global Instance isequivs_prod A B `{HasEquivs A} `{HasEquivs B}
       {a1 a2 : A} {b1 b2 : B} {f : a1 $-> a2} {g : b1 $-> b2}
       {ef : CatIsEquiv f} {eg : CatIsEquiv g}
  : @CatIsEquiv (A*B) _ _ _ _ _ (a1,b1) (a2,b2) (f,g) := (ef,eg).

(** ** Product functors *)

Global Instance is0functor_prod_functor {A B C D : Type}
  (F : A -> B) (G : C -> D) `{Is0Functor _ _ F, Is0Functor _ _ G}
  : Is0Functor (functor_prod F G).
A, B, C, D: Type
F: A -> B
G: C -> D
H: IsGraph A
H0: IsGraph B
H1: Is0Functor F
H2: IsGraph C
H3: IsGraph D
H4: Is0Functor G
Is0Functor (functor_prod F G)
Proof.
A, B, C, D: Type
F: A -> B
G: C -> D
H: IsGraph A
H0: IsGraph B
H1: Is0Functor F
H2: IsGraph C
H3: IsGraph D
H4: Is0Functor G
Is0Functor (functor_prod F G)
  apply Build_Is0Functor.
A, B, C, D: Type
F: A -> B
G: C -> D
H: IsGraph A
H0: IsGraph B
H1: Is0Functor F
H2: IsGraph C
H3: IsGraph D
H4: Is0Functor G
forall a b : A * C,
(a $-> b) -> functor_prod F G a $-> functor_prod F G b
  intros [a1 c1] [a2 c2] [f g].
A, B, C, D: Type
F: A -> B
G: C -> D
H: IsGraph A
H0: IsGraph B
H1: Is0Functor F
H2: IsGraph C
H3: IsGraph D
H4: Is0Functor G
a1: A
c1: C
a2: A
c2: C
f: fst (a1, c1) $-> fst (a2, c2)
g: snd (a1, c1) $-> snd (a2, c2)
functor_prod F G (a1, c1) $->
functor_prod F G (a2, c2)
  exact (fmap F f , fmap G g).
Defined.

Global Instance is1functor_prod_functor {A B C D : Type}
  (F : A -> B) (G : C -> D) `{Is1Functor _ _ F, Is1Functor _ _ G}
  : Is1Functor (functor_prod F G).
A, B, C, D: Type
F: A -> B
G: C -> D
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H3: Is1Cat D
Is0Functor1: Is0Functor G
H4: Is1Functor G
Is1Functor (functor_prod F G)
Proof.
A, B, C, D: Type
F: A -> B
G: C -> D
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H3: Is1Cat D
Is0Functor1: Is0Functor G
H4: Is1Functor G
Is1Functor (functor_prod F G)
  apply Build_Is1Functor.
A, B, C, D: Type
F: A -> B
G: C -> D
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H3: Is1Cat D
Is0Functor1: Is0Functor G
H4: Is1Functor G
forall (a b : A * C) (f g : a $-> b),
f $== g ->
fmap (functor_prod F G) f $==
fmap (functor_prod F G) g
A, B, C, D: Type
F: A -> B
G: C -> D
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H3: Is1Cat D
Is0Functor1: Is0Functor G
H4: Is1Functor G
forall a : A * C,
fmap (functor_prod F G) (Id a) $==
Id (functor_prod F G a)
A, B, C, D: Type
F: A -> B
G: C -> D
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H3: Is1Cat D
Is0Functor1: Is0Functor G
H4: Is1Functor G
forall (a b c : A * C) 
(f : a $-> b) (g : b $-> c),
fmap (functor_prod F G) (g $o f) $==
fmap (functor_prod F G) g $o fmap (functor_prod F G) f
  -
A, B, C, D: Type
F: A -> B
G: C -> D
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H3: Is1Cat D
Is0Functor1: Is0Functor G
H4: Is1Functor G
forall (a b : A * C) (f g : a $-> b),
f $== g ->
fmap (functor_prod F G) f $==
fmap (functor_prod F G) g intros [a1 c1] [a2 c2] [f1 g1] [f2 g2] [p q].
A, B, C, D: Type
F: A -> B
G: C -> D
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H3: Is1Cat D
Is0Functor1: Is0Functor G
H4: Is1Functor G
a1: A
c1: C
a2: A
c2: C
f1: fst (a1, c1) $-> fst (a2, c2)
g1: snd (a1, c1) $-> snd (a2, c2)
f2: fst (a1, c1) $-> fst (a2, c2)
g2: snd (a1, c1) $-> snd (a2, c2)
p: fst (f1, g1) $-> fst (f2, g2)
q: snd (f1, g1) $-> snd (f2, g2)
fmap (functor_prod F G) (f1, g1) $==
fmap (functor_prod F G) (f2, g2)
    exact (fmap2 F p , fmap2 G q).
  -
A, B, C, D: Type
F: A -> B
G: C -> D
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H3: Is1Cat D
Is0Functor1: Is0Functor G
H4: Is1Functor G
forall a : A * C,
fmap (functor_prod F G) (Id a) $==
Id (functor_prod F G a) intros [a c].
A, B, C, D: Type
F: A -> B
G: C -> D
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H3: Is1Cat D
Is0Functor1: Is0Functor G
H4: Is1Functor G
a: A
c: C
fmap (functor_prod F G) (Id (a, c)) $==
Id (functor_prod F G (a, c))
    exact (fmap_id F a, fmap_id G c).
  -
A, B, C, D: Type
F: A -> B
G: C -> D
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H3: Is1Cat D
Is0Functor1: Is0Functor G
H4: Is1Functor G
forall (a b c : A * C) 
(f : a $-> b) (g : b $-> c),
fmap (functor_prod F G) (g $o f) $==
fmap (functor_prod F G) g $o fmap (functor_prod F G) f intros [a1 c1] [a2 c2] [a3 c3] [f1 g1] [f2 g2].
A, B, C, D: Type
F: A -> B
G: C -> D
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
IsGraph1: IsGraph B
Is2Graph1: Is2Graph B
Is01Cat1: Is01Cat B
H0: Is1Cat B
Is0Functor0: Is0Functor F
H1: Is1Functor F
IsGraph2: IsGraph C
Is2Graph2: Is2Graph C
Is01Cat2: Is01Cat C
H2: Is1Cat C
IsGraph3: IsGraph D
Is2Graph3: Is2Graph D
Is01Cat3: Is01Cat D
H3: Is1Cat D
Is0Functor1: Is0Functor G
H4: Is1Functor G
a1: A
c1: C
a2: A
c2: C
a3: A
c3: C
f1: fst (a1, c1) $-> fst (a2, c2)
g1: snd (a1, c1) $-> snd (a2, c2)
f2: fst (a2, c2) $-> fst (a3, c3)
g2: snd (a2, c2) $-> snd (a3, c3)
fmap (functor_prod F G) ((f2, g2) $o (f1, g1)) $==
fmap (functor_prod F G) (f2, g2) $o
fmap (functor_prod F G) (f1, g1)
    exact (fmap_comp F f1 f2 , fmap_comp G g1 g2).
Defined.

Global Instance is0functor_fst {A B : Type} `{!IsGraph A, !IsGraph B}
  : Is0Functor (@fst A B).
A, B: Type
IsGraph0: IsGraph A
IsGraph1: IsGraph B
Is0Functor fst
Proof.
A, B: Type
IsGraph0: IsGraph A
IsGraph1: IsGraph B
Is0Functor fst
  apply Build_Is0Functor.
A, B: Type
IsGraph0: IsGraph A
IsGraph1: IsGraph B
forall a b : A * B, (a $-> b) -> fst a $-> fst b
  intros ? ? f; exact (fst f).
Defined.

Global Instance is0functor_snd {A B : Type} `{!IsGraph A, !IsGraph B}
  : Is0Functor (@snd A B).
A, B: Type
IsGraph0: IsGraph A
IsGraph1: IsGraph B
Is0Functor snd
Proof.
A, B: Type
IsGraph0: IsGraph A
IsGraph1: IsGraph B
Is0Functor snd
  apply Build_Is0Functor.
A, B: Type
IsGraph0: IsGraph A
IsGraph1: IsGraph B
forall a b : A * B, (a $-> b) -> snd a $-> snd b
  intros ? ? f; exact (snd f).
Defined.

(** Swap functor *)

Global Instance is0functor_equiv_prod_symm {A B : Type} `{IsGraph A, IsGraph B}
  : Is0Functor (equiv_prod_symm A B).
A, B: Type
H: IsGraph A
H0: IsGraph B
Is0Functor (equiv_prod_symm A B)
Proof.
A, B: Type
H: IsGraph A
H0: IsGraph B
Is0Functor (equiv_prod_symm A B)
  snrapply Build_Is0Functor.
A, B: Type
H: IsGraph A
H0: IsGraph B
forall a b : A * B,
(a $-> b) ->
equiv_prod_symm A B a $-> equiv_prod_symm A B b
  intros a b.
A, B: Type
H: IsGraph A
H0: IsGraph B
a, b: A * B
(a $-> b) ->
equiv_prod_symm A B a $-> equiv_prod_symm A B b
  apply equiv_prod_symm.
Defined.

Global Instance is1functor_equiv_prod_symm {A B : Type} `{Is1Cat A, Is1Cat B}
  : Is1Functor (equiv_prod_symm A B).
A, B: 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
Is1Functor (equiv_prod_symm A B)
Proof.
A, B: 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
Is1Functor (equiv_prod_symm A B)
  snrapply Build_Is1Functor.
A, B: 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
forall (a b : A * B) (f g : a $-> b),
f $== g ->
fmap (equiv_prod_symm A B) f $==
fmap (equiv_prod_symm A B) g
A, B: 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
forall a : A * B,
fmap (equiv_prod_symm A B) (Id a) $==
Id (equiv_prod_symm A B a)
A, B: 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
forall (a b c : A * B) 
(f : a $-> b) (g : b $-> c),
fmap (equiv_prod_symm A B) (g $o f) $==
fmap (equiv_prod_symm A B) g $o
fmap (equiv_prod_symm A B) f
  -
A, B: 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
forall (a b : A * B) (f g : a $-> b),
f $== g ->
fmap (equiv_prod_symm A B) f $==
fmap (equiv_prod_symm A B) g intros a b f g.
A, B: 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
a, b: A * B
f, g: a $-> b
f $== g ->
fmap (equiv_prod_symm A B) f $==
fmap (equiv_prod_symm A B) g
    apply equiv_prod_symm.
  -
A, B: 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
forall a : A * B,
fmap (equiv_prod_symm A B) (Id a) $==
Id (equiv_prod_symm A B a) intros a.
A, B: 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
a: A * B
fmap (equiv_prod_symm A B) (Id a) $==
Id (equiv_prod_symm A B a)
    reflexivity.
  -
A, B: 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
forall (a b c : A * B) 
(f : a $-> b) (g : b $-> c),
fmap (equiv_prod_symm A B) (g $o f) $==
fmap (equiv_prod_symm A B) g $o
fmap (equiv_prod_symm A B) f reflexivity.
Defined.

(** Inclusions into a product category are functorial. *)

Global Instance is0functor_prod_include10 {A B : Type} `{IsGraph A, Is01Cat B}
  (b : B)
  : Is0Functor (fun a : A => (a, b)).
A, B: Type
H: IsGraph A
H0: IsGraph B
H1: Is01Cat B
b: B
Is0Functor (fun a : A => (a, b))
Proof.
A, B: Type
H: IsGraph A
H0: IsGraph B
H1: Is01Cat B
b: B
Is0Functor (fun a : A => (a, b))
  nrapply Build_Is0Functor.
A, B: Type
H: IsGraph A
H0: IsGraph B
H1: Is01Cat B
b: B
forall a b0 : A, (a $-> b0) -> (a, b) $-> (b0, b)
  intros a c f.
A, B: Type
H: IsGraph A
H0: IsGraph B
H1: Is01Cat B
b: B
a, c: A
f: a $-> c
(a, b) $-> (c, b)
  exact (f, Id b).
Defined.

Global Instance is1functor_prod_include10 {A B : Type} `{Is1Cat A, Is1Cat B}
  (b : B)
  : Is1Functor (fun a : A => (a, b)).
A, B: 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
b: B
Is1Functor (fun a : A => (a, b))
Proof.
A, B: 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
b: B
Is1Functor (fun a : A => (a, b))
  nrapply Build_Is1Functor.
A, B: 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
b: B
forall (a b0 : A) (f g : a $-> b0),
f $== g ->
fmap (fun a0 : A => (a0, b)) f $==
fmap (fun a0 : A => (a0, b)) g
A, B: 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
b: B
forall a : A,
fmap (fun a0 : A => (a0, b)) (Id a) $== Id (a, b)
A, B: 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
b: B
forall (a b0 c : A) (f : a $-> b0) 
(g : b0 $-> c),
fmap (fun a0 : A => (a0, b)) (g $o f) $==
fmap (fun a0 : A => (a0, b)) g $o
fmap (fun a0 : A => (a0, b)) f
  -
A, B: 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
b: B
forall (a b0 : A) (f g : a $-> b0),
f $== g ->
fmap (fun a0 : A => (a0, b)) f $==
fmap (fun a0 : A => (a0, b)) g intros a c f g p.
A, B: 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
b: B
a, c: A
f, g: a $-> c
p: f $== g
fmap (fun a : A => (a, b)) f $==
fmap (fun a : A => (a, b)) g
    exact (p, Id _).
  -
A, B: 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
b: B
forall a : A,
fmap (fun a0 : A => (a0, b)) (Id a) $== Id (a, b) intros a; reflexivity.
  -
A, B: 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
b: B
forall (a b0 c : A) (f : a $-> b0) 
(g : b0 $-> c),
fmap (fun a0 : A => (a0, b)) (g $o f) $==
fmap (fun a0 : A => (a0, b)) g $o
fmap (fun a0 : A => (a0, b)) f intros a c d f g.
A, B: 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
b: B
a, c, d: A
f: a $-> c
g: c $-> d
fmap (fun a : A => (a, b)) (g $o f) $==
fmap (fun a : A => (a, b)) g $o
fmap (fun a : A => (a, b)) f
    exact (Id _, (cat_idl _)^$).
Defined.

Global Instance is0functor_prod_include01 {A B : Type} `{Is01Cat A, IsGraph B}
  (a : A)
  : Is0Functor (fun b : B => (a, b)).
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
a: A
Is0Functor (fun b : B => (a, b))
Proof.
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
a: A
Is0Functor (fun b : B => (a, b))
  nrapply Build_Is0Functor.
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
a: A
forall a0 b : B, (a0 $-> b) -> (a, a0) $-> (a, b)
  intros b c f.
A, B: Type
H: IsGraph A
H0: Is01Cat A
H1: IsGraph B
a: A
b, c: B
f: b $-> c
(a, b) $-> (a, c)
  exact (Id a, f).
Defined.

Global Instance is1functor_prod_include01 {A B : Type} `{Is1Cat A, Is1Cat B}
  (a : A)
  : Is1Functor (fun b : B => (a, b)).
A, B: 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
a: A
Is1Functor (fun b : B => (a, b))
Proof.
A, B: 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
a: A
Is1Functor (fun b : B => (a, b))
  nrapply Build_Is1Functor.
A, B: 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
a: A
forall (a0 b : B) (f g : a0 $-> b),
f $== g ->
fmap (fun b0 : B => (a, b0)) f $==
fmap (fun b0 : B => (a, b0)) g
A, B: 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
a: A
forall a0 : B,
fmap (fun b : B => (a, b)) (Id a0) $== Id (a, a0)
A, B: 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
a: A
forall (a0 b c : B) (f : a0 $-> b) 
(g : b $-> c),
fmap (fun b0 : B => (a, b0)) (g $o f) $==
fmap (fun b0 : B => (a, b0)) g $o
fmap (fun b0 : B => (a, b0)) f
  -
A, B: 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
a: A
forall (a0 b : B) (f g : a0 $-> b),
f $== g ->
fmap (fun b0 : B => (a, b0)) f $==
fmap (fun b0 : B => (a, b0)) g intros b c f g p.
A, B: 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
a: A
b, c: B
f, g: b $-> c
p: f $== g
fmap (fun b : B => (a, b)) f $==
fmap (fun b : B => (a, b)) g
    exact (Id _, p).
  -
A, B: 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
a: A
forall a0 : B,
fmap (fun b : B => (a, b)) (Id a0) $== Id (a, a0) intros b; reflexivity.
  -
A, B: 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
a: A
forall (a0 b c : B) (f : a0 $-> b) 
(g : b $-> c),
fmap (fun b0 : B => (a, b0)) (g $o f) $==
fmap (fun b0 : B => (a, b0)) g $o
fmap (fun b0 : B => (a, b0)) f intros b c d f g.
A, B: 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
a: A
b, c, d: B
f: b $-> c
g: c $-> d
fmap (fun b : B => (a, b)) (g $o f) $==
fmap (fun b : B => (a, b)) g $o
fmap (fun b : B => (a, b)) f
    exact ((cat_idl _)^$, Id _).
Defined.

(** Functors from a product category are functorial in each argument *)

Global Instance is0functor_functor_uncurried01 {A B C : Type}
  `{Is01Cat A, IsGraph B, IsGraph C}
  (F : A * B -> C) `{!Is0Functor F} (a : A)
  : Is0Functor (fun b => F (a, b))
  := is0functor_compose (fun b => (a, b)) F.

Global Instance is1functor_functor_uncurried01 {A B C : Type}
  `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F} (a : A)
  : Is1Functor (fun b => F (a, b))
  := is1functor_compose (fun b => (a, b)) F.

Global Instance is0functor_functor_uncurried10 {A B C : Type}
  `{IsGraph A, Is01Cat B, IsGraph C}
  (F : A * B -> C) `{!Is0Functor F} (b : B)
  : Is0Functor (fun a => F (a, b))
  := is0functor_compose (fun a => (a, b)) F.

Global Instance is1functor_functor_uncurried10 {A B C : Type}
  `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F} (b : B)
  : Is1Functor (fun a => F (a, b))
  := is1functor_compose (fun a => (a, b)) F.

(** Conversely, if [F : A * B -> C] is a 0-functor in each variable, then it is a 0-functor. *)
Definition is0functor_prod_is0functor {A B C : Type}
  `{IsGraph A, IsGraph B, Is01Cat C} (F : A * B -> C)
  `{!forall a, Is0Functor (fun b => F (a,b)), !forall b, Is0Functor (fun a => F (a,b))}
  : Is0Functor 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 (fun b : B => F (a, b))
H4: forall b : B, Is0Functor (fun a : A => F (a, b))
Is0Functor 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 (fun b : B => F (a, b))
H4: forall b : B, Is0Functor (fun a : A => F (a, b))
Is0Functor F
  snrapply Build_Is0Functor.
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 (fun b : B => F (a, b))
H4: forall b : B, Is0Functor (fun a : A => F (a, b))
forall a b : A * B, (a $-> b) -> F a $-> F b
  intros [a b] [a' b'] [f g].
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 (fun b : B => F (a, b))
H4: forall b : B, Is0Functor (fun a : A => F (a, b))
a: A
b: B
a': A
b': B
f: fst (a, b) $-> fst (a', b')
g: snd (a, b) $-> snd (a', b')
F (a, b) $-> F (a', b')
  exact (fmap (fun a0 => F (a0,b')) f $o fmap (fun b0 => F (a,b0)) g).
Defined.
(** TODO: If we make this an instance, will it cause typeclass search to spin? *)
Hint Immediate is0functor_prod_is0functor : typeclass_instances.

(** And if [F : A * B -> C] is a 1-functor in each variable and satisfies a coherence, then it is a 1-functor. *)
Definition is1functor_prod_is1functor {A B C : Type}
  `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A * B -> C)
  `{!forall a, Is0Functor (fun b => F (a,b)), !forall b, Is0Functor (fun a => F (a,b))}
  `{!forall a, Is1Functor (fun b => F (a,b)), !forall b, Is1Functor (fun a => F (a,b))}
  (bifunctor_coh : forall a0 a1 (f : a0 $-> a1) b0 b1 (g : b0 $-> b1),
    fmap (fun b => F (a1,b)) g $o fmap (fun a => F (a,b0)) f
      $== fmap (fun a => F(a,b1)) f $o fmap (fun b => F (a0,b)) g)
  : Is1Functor 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 (fun b : B => F (a, b))
H3: forall b : B, Is0Functor (fun a : A => F (a, b))
H4: forall a : A, Is1Functor (fun b : B => F (a, b))
H5: forall b : B, Is1Functor (fun a : A => F (a, b))
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap (fun b : B => F (a1, b)) g $o
fmap (fun a : A => F (a, b0)) f $==
fmap (fun a : A => F (a, b1)) f $o
fmap (fun b : B => F (a0, b)) g
Is1Functor 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 (fun b : B => F (a, b))
H3: forall b : B, Is0Functor (fun a : A => F (a, b))
H4: forall a : A, Is1Functor (fun b : B => F (a, b))
H5: forall b : B, Is1Functor (fun a : A => F (a, b))
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap (fun b : B => F (a1, b)) g $o
fmap (fun a : A => F (a, b0)) f $==
fmap (fun a : A => F (a, b1)) f $o
fmap (fun b : B => F (a0, b)) g
Is1Functor F
  snrapply Build_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 (fun b : B => F (a, b))
H3: forall b : B, Is0Functor (fun a : A => F (a, b))
H4: forall a : A, Is1Functor (fun b : B => F (a, b))
H5: forall b : B, Is1Functor (fun a : A => F (a, b))
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap (fun b : B => F (a1, b)) g $o
fmap (fun a : A => F (a, b0)) f $==
fmap (fun a : A => F (a, b1)) f $o
fmap (fun b : B => F (a0, b)) g
forall (a b : A * B) (f g : a $-> b),
f $== g -> fmap F f $== fmap 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
H2: forall a : A, Is0Functor (fun b : B => F (a, b))
H3: forall b : B, Is0Functor (fun a : A => F (a, b))
H4: forall a : A, Is1Functor (fun b : B => F (a, b))
H5: forall b : B, Is1Functor (fun a : A => F (a, b))
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap (fun b : B => F (a1, b)) g $o
fmap (fun a : A => F (a, b0)) f $==
fmap (fun a : A => F (a, b1)) f $o
fmap (fun b : B => F (a0, b)) g
forall a : A * B, fmap F (Id a) $== Id (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 (fun b : B => F (a, b))
H3: forall b : B, Is0Functor (fun a : A => F (a, b))
H4: forall a : A, Is1Functor (fun b : B => F (a, b))
H5: forall b : B, Is1Functor (fun a : A => F (a, b))
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap (fun b : B => F (a1, b)) g $o
fmap (fun a : A => F (a, b0)) f $==
fmap (fun a : A => F (a, b1)) f $o
fmap (fun b : B => F (a0, b)) g
forall (a b c : A * B) 
(f : a $-> b) (g : b $-> c),
fmap F (g $o f) $== fmap F g $o fmap 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
H2: forall a : A, Is0Functor (fun b : B => F (a, b))
H3: forall b : B, Is0Functor (fun a : A => F (a, b))
H4: forall a : A, Is1Functor (fun b : B => F (a, b))
H5: forall b : B, Is1Functor (fun a : A => F (a, b))
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap (fun b : B => F (a1, b)) g $o
fmap (fun a : A => F (a, b0)) f $==
fmap (fun a : A => F (a, b1)) f $o
fmap (fun b : B => F (a0, b)) g
forall (a b : A * B) (f g : a $-> b),
f $== g -> fmap F f $== fmap F g intros [a b] [a' b'] [f g] [f' g'] [p p']; unfold fst, snd 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
H2: forall a : A, Is0Functor (fun b : B => F (a, b))
H3: forall b : B, Is0Functor (fun a : A => F (a, b))
H4: forall a : A, Is1Functor (fun b : B => F (a, b))
H5: forall b : B, Is1Functor (fun a : A => F (a, b))
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap (fun b : B => F (a1, b)) g $o
fmap (fun a : A => F (a, b0)) f $==
fmap (fun a : A => F (a, b1)) f $o
fmap (fun b : B => F (a0, b)) g
a: A
b: B
a': A
b': B
f: a $-> a'
g: b $-> b'
f': a $-> a'
g': b $-> b'
p: f $-> f'
p': g $-> g'
fmap F (f, g) $== fmap F (f', g')
    exact (fmap2 (fun b0 => F (a,b0)) p' $@@ fmap2 (fun a0 => F (a0,b')) p).
  -
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 (fun b : B => F (a, b))
H3: forall b : B, Is0Functor (fun a : A => F (a, b))
H4: forall a : A, Is1Functor (fun b : B => F (a, b))
H5: forall b : B, Is1Functor (fun a : A => F (a, b))
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap (fun b : B => F (a1, b)) g $o
fmap (fun a : A => F (a, b0)) f $==
fmap (fun a : A => F (a, b1)) f $o
fmap (fun b : B => F (a0, b)) g
forall a : A * B, fmap F (Id a) $== Id (F a) intros [a 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 (fun b : B => F (a, b))
H3: forall b : B, Is0Functor (fun a : A => F (a, b))
H4: forall a : A, Is1Functor (fun b : B => F (a, b))
H5: forall b : B, Is1Functor (fun a : A => F (a, b))
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap (fun b : B => F (a1, b)) g $o
fmap (fun a : A => F (a, b0)) f $==
fmap (fun a : A => F (a, b1)) f $o
fmap (fun b : B => F (a0, b)) g
a: A
b: B
fmap F (Id (a, b)) $== Id (F (a, b))
    exact ((fmap_id (fun b0 => F (a,b0)) b $@@ fmap_id (fun a0 => F (a0,b)) _) $@ 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
H2: forall a : A, Is0Functor (fun b : B => F (a, b))
H3: forall b : B, Is0Functor (fun a : A => F (a, b))
H4: forall a : A, Is1Functor (fun b : B => F (a, b))
H5: forall b : B, Is1Functor (fun a : A => F (a, b))
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap (fun b : B => F (a1, b)) g $o
fmap (fun a : A => F (a, b0)) f $==
fmap (fun a : A => F (a, b1)) f $o
fmap (fun b : B => F (a0, b)) g
forall (a b c : A * B) 
(f : a $-> b) (g : b $-> c),
fmap F (g $o f) $== fmap F g $o fmap F f intros [a b] [a' b'] [a'' b''] [f g] [f' g']; unfold fst, snd 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
H2: forall a : A, Is0Functor (fun b : B => F (a, b))
H3: forall b : B, Is0Functor (fun a : A => F (a, b))
H4: forall a : A, Is1Functor (fun b : B => F (a, b))
H5: forall b : B, Is1Functor (fun a : A => F (a, b))
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap (fun b : B => F (a1, b)) g $o
fmap (fun a : A => F (a, b0)) f $==
fmap (fun a : A => F (a, b1)) f $o
fmap (fun b : B => F (a0, b)) g
a: A
b: B
a': A
b': B
a'': A
b'': B
f: a $-> a'
g: b $-> b'
f': a' $-> a''
g': b' $-> b''
fmap F ((f', g') $o (f, g)) $==
fmap F (f', g') $o fmap F (f, g)
    refine ((fmap_comp (fun b0 => F (a,b0)) g g' $@@ fmap_comp (fun a0 => F (a0,b'')) 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
H2: forall a : A, Is0Functor (fun b : B => F (a, b))
H3: forall b : B, Is0Functor (fun a : A => F (a, b))
H4: forall a : A, Is1Functor (fun b : B => F (a, b))
H5: forall b : B, Is1Functor (fun a : A => F (a, b))
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap (fun b : B => F (a1, b)) g $o
fmap (fun a : A => F (a, b0)) f $==
fmap (fun a : A => F (a, b1)) f $o
fmap (fun b : B => F (a0, b)) g
a: A
b: B
a': A
b': B
a'': A
b'': B
f: a $-> a'
g: b $-> b'
f': a' $-> a''
g': b' $-> b''
fmap (fun a : A => F (a, b'')) f' $o
fmap (fun a : A => F (a, b'')) f $o
(fmap (fun b : B => F (a, b)) g' $o
 fmap (fun b : B => F (a, b)) g) $==
fmap F (f', g') $o fmap F (f, g)
    nrefine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ cat_assoc _ _ _).
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 (fun b : B => F (a, b))
H3: forall b : B, Is0Functor (fun a : A => F (a, b))
H4: forall a : A, Is1Functor (fun b : B => F (a, b))
H5: forall b : B, Is1Functor (fun a : A => F (a, b))
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap (fun b : B => F (a1, b)) g $o
fmap (fun a : A => F (a, b0)) f $==
fmap (fun a : A => F (a, b1)) f $o
fmap (fun b : B => F (a0, b)) g
a: A
b: B
a': A
b': B
a'': A
b'': B
f: a $-> a'
g: b $-> b'
f': a' $-> a''
g': b' $-> b''
fmap (fun a : A => F (a, b'')) f' $o
fmap (fun a : A => F (a, b'')) f $o
fmap (fun b : B => F (a, b)) g' $==
fmap F (f', g') $o fmap (fun a : A => F (a, b')) f
    refine (cat_assoc _ _ _ $@ (_ $@L _^$) $@ cat_assoc_opp _ _ _).
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 (fun b : B => F (a, b))
H3: forall b : B, Is0Functor (fun a : A => F (a, b))
H4: forall a : A, Is1Functor (fun b : B => F (a, b))
H5: forall b : B, Is1Functor (fun a : A => F (a, b))
bifunctor_coh: forall (a0 a1 : A) (f : a0 $-> a1)
(b0 b1 : B) (g : b0 $-> b1),
fmap (fun b : B => F (a1, b)) g $o
fmap (fun a : A => F (a, b0)) f $==
fmap (fun a : A => F (a, b1)) f $o
fmap (fun b : B => F (a0, b)) g
a: A
b: B
a': A
b': B
a'': A
b'': B
f: a $-> a'
g: b $-> b'
f': a' $-> a''
g': b' $-> b''
fmap (fun b : B => F (a', b)) g' $o
fmap (fun a : A => F (a, b')) f $->
fmap (fun a : A => F (a, b'')) f $o
fmap (fun b : B => F (a, b)) g'
    nrapply bifunctor_coh.
Defined.
Hint Immediate is1functor_prod_is1functor : typeclass_instances.

(** Applies a two variable functor via uncurrying. Note that the precondition on [C] is slightly weaker than that of [Bifunctor.fmap11]. *)
Definition fmap11_uncurry {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
  (F : A -> B -> C) {H2 : Is0Functor (uncurry F)}
  {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)
  : F a0 b0 $-> F a1 b1
  := @fmap _ _ _ _ (uncurry F) H2 (a0, b0) (a1, b1) (f, g).

Definition fmap_pair {A B C : Type}  
  `{IsGraph A, IsGraph B, IsGraph C}  
  (F : A * B -> C) `{!Is0Functor F}  
  {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)  
  : F (a0, b0) $-> F (a1, b1)  
  := fmap (a := (a0, b0)) (b := (a1, b1)) F (f, g).  

Definition fmap_pair_comp {A B C : Type}  
  `{Is1Cat A, Is1Cat B, Is1Cat C}  
  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F}  
  {a0 a1 a2 : A} {b0 b1 b2 : B}
  (f : a0 $-> a1) (h : b0 $-> b1) (g : a1 $-> a2) (i : b1 $-> b2)  
  : fmap_pair F (g $o f) (i $o h)
    $== fmap_pair F g i $o fmap_pair F f h
  := fmap_comp (a := (a0, b0)) (b := (a1, b1)) (c := (a2, b2)) F (f, h) (g, i).

Definition fmap2_pair {A B C : Type}
  `{Is1Cat A, Is1Cat B, Is1Cat C}
  (F : A * B -> C) `{!Is0Functor F, !Is1Functor F}
  {a0 a1 : A} {f f' : a0 $-> a1} (p : f $== f')
  {b0 b1 : B} {g g' : b0 $-> b1} (q : g $== g')
  : fmap_pair F f g $== fmap_pair F f' g'
  := fmap2 F (a := (a0, b0)) (b := (a1, b1)) (f := (f, g)) (g := (f' ,g')) (p, q).