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

(** ** Sum categories *)

Instance isgraph_sum A B `{IsGraph A} `{IsGraph B}
  : IsGraph (A + B).
A, B: Type
H: IsGraph A
H0: IsGraph B
IsGraph (A + B)
Proof.
A, B: Type
H: IsGraph A
H0: IsGraph B
IsGraph (A + B)
  econstructor.
A, B: Type
H: IsGraph A
H0: IsGraph B
A + B -> A + B -> Type
  intros [a1 | b1] [a2 | b2].
A, B: Type
H: IsGraph A
H0: IsGraph B
a1, a2: A
Type
A, B: Type
H: IsGraph A
H0: IsGraph B
a1: A
b2: B
Type
A, B: Type
H: IsGraph A
H0: IsGraph B
b1: B
a2: A
Type
A, B: Type
H: IsGraph A
H0: IsGraph B
b1, b2: B
Type
  +
A, B: Type
H: IsGraph A
H0: IsGraph B
a1, a2: A
Type exact (a1 $-> a2).
  +
A, B: Type
H: IsGraph A
H0: IsGraph B
a1: A
b2: B
Type exact Empty.
  +
A, B: Type
H: IsGraph A
H0: IsGraph B
b1: B
a2: A
Type exact Empty.
  +
A, B: Type
H: IsGraph A
H0: IsGraph B
b1, b2: B
Type exact (b1 $-> b2).
Defined.

Instance is01cat_sum 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)
  srapply Build_Is01Cat.
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]; cbn; apply Id.
  -
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 [a | b] [a1 | b1] [a2 | b2];
    try contradiction; cbn; exact cat_comp.
Defined.

Instance is2graph_sum 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 x y; apply Build_IsGraph.
A, B: Type
H: IsGraph A
H0: Is2Graph A
H1: IsGraph B
H2: Is2Graph B
x, y: A + B
(x $-> y) -> (x $-> y) -> Type
  destruct x as [a1 | b1], y as [a2 | b2];
  try contradiction; cbn; exact Hom.
Defined.

(* Note: [try contradiction] deals with empty cases. *)
Instance is1cat_sum 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)
  snapply 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 : A + B, Is01Cat (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
forall a b : A + B, Is0Gpd (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
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 : A + B, Is01Cat (a $-> b) intros x y.
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
x, y: A + B
Is01Cat (x $-> y)
    srapply Build_Is01Cat; destruct x as [a1 | b1], y as [a2 | b2].
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, a2: A
forall a : inl a1 $-> inl a2, a $-> 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
a1: A
b2: B
forall a : inl a1 $-> inr b2, a $-> 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
b1: B
a2: A
forall a : inr b1 $-> inl a2, a $-> 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
b1, b2: B
forall a : inr b1 $-> inr b2, a $-> 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
a1, a2: A
forall a b c : inl a1 $-> inl a2,
(b $-> c) -> (a $-> b) -> a $-> c
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
b2: B
forall a b c : inl a1 $-> inr b2,
(b $-> c) -> (a $-> b) -> a $-> c
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
b1: B
a2: A
forall a b c : inr b1 $-> inl a2,
(b $-> c) -> (a $-> b) -> a $-> c
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
b1, b2: B
forall a b c : inr b1 $-> inr b2,
(b $-> c) -> (a $-> b) -> a $-> c
    2,3,6,7: contradiction.
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, a2: A
forall a : inl a1 $-> inl a2, a $-> 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
b1, b2: B
forall a : inr b1 $-> inr b2, a $-> 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
a1, a2: A
forall a b c : inl a1 $-> inl a2,
(b $-> c) -> (a $-> b) -> a $-> c
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
b1, b2: B
forall a b c : inr b1 $-> inr b2,
(b $-> c) -> (a $-> b) -> a $-> c
    all: cbn.
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, a2: A
forall a : a1 $-> a2, a $-> 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
b1, b2: B
forall a : b1 $-> b2, a $-> 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
a1, a2: A
forall a b c : a1 $-> a2,
(b $-> c) -> (a $-> b) -> a $-> c
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
b1, b2: B
forall a b c : b1 $-> b2,
(b $-> c) -> (a $-> b) -> a $-> c
    1,2: exact 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
a1, a2: A
forall a b c : a1 $-> a2,
(b $-> c) -> (a $-> b) -> a $-> c
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
b1, b2: B
forall a b c : b1 $-> b2,
(b $-> c) -> (a $-> b) -> a $-> c
    1,2: intros a b c; exact cat_comp.
  -
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, Is0Gpd (a $-> b) intros x y; srapply Build_Is0Gpd.
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
x, y: A + B
forall a b : x $-> y, (a $-> b) -> b $-> a
    destruct x as [a1 | b1], y as [a2 | b2].
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, a2: A
forall a b : inl a1 $-> inl a2, (a $-> b) -> 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
a1: A
b2: B
forall a b : inl a1 $-> inr b2, (a $-> b) -> 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
b1: B
a2: A
forall a b : inr b1 $-> inl a2, (a $-> b) -> 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
b1, b2: B
forall a b : inr b1 $-> inr b2, (a $-> b) -> b $-> a
    2,3: contradiction.
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, a2: A
forall a b : inl a1 $-> inl a2, (a $-> b) -> 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
b1, b2: B
forall a b : inr b1 $-> inr b2, (a $-> b) -> b $-> a
    all: cbn; intros f g; exact gpd_rev.
  -
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 x y z h; 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
x, y, z: A + B
h: y $-> z
forall a b : x $-> y,
(a $-> b) -> cat_postcomp x h a $-> cat_postcomp x h b
    intros 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
x, y, z: A + B
h: y $-> z
f, g: x $-> y
p: f $-> g
cat_postcomp x h f $-> cat_postcomp x h g
    destruct x as [a1 | b1], y as [a2 | b2].
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, a2: A
z: A + B
h: inl a2 $-> z
f, g: inl a1 $-> inl a2
p: f $-> g
cat_postcomp (inl a1) h f $->
cat_postcomp (inl a1) h 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
a1: A
b2: B
z: A + B
h: inr b2 $-> z
f, g: inl a1 $-> inr b2
p: f $-> g
cat_postcomp (inl a1) h f $->
cat_postcomp (inl a1) h 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
b1: B
a2: A
z: A + B
h: inl a2 $-> z
f, g: inr b1 $-> inl a2
p: f $-> g
cat_postcomp (inr b1) h f $->
cat_postcomp (inr b1) h 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
b1, b2: B
z: A + B
h: inr b2 $-> z
f, g: inr b1 $-> inr b2
p: f $-> g
cat_postcomp (inr b1) h f $->
cat_postcomp (inr b1) h g
    2,3: contradiction.
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, a2: A
z: A + B
h: inl a2 $-> z
f, g: inl a1 $-> inl a2
p: f $-> g
cat_postcomp (inl a1) h f $->
cat_postcomp (inl a1) h 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
b1, b2: B
z: A + B
h: inr b2 $-> z
f, g: inr b1 $-> inr b2
p: f $-> g
cat_postcomp (inr b1) h f $->
cat_postcomp (inr b1) h g
    all: destruct z as [a3 | b3].
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, a2, a3: A
h: inl a2 $-> inl a3
f, g: inl a1 $-> inl a2
p: f $-> g
cat_postcomp (inl a1) h f $->
cat_postcomp (inl a1) h 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
a1, a2: A
b3: B
h: inl a2 $-> inr b3
f, g: inl a1 $-> inl a2
p: f $-> g
cat_postcomp (inl a1) h f $->
cat_postcomp (inl a1) h 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
b1, b2: B
a3: A
h: inr b2 $-> inl a3
f, g: inr b1 $-> inr b2
p: f $-> g
cat_postcomp (inr b1) h f $->
cat_postcomp (inr b1) h 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
b1, b2, b3: B
h: inr b2 $-> inr b3
f, g: inr b1 $-> inr b2
p: f $-> g
cat_postcomp (inr b1) h f $->
cat_postcomp (inr b1) h g
    2,3: contradiction.
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, a2, a3: A
h: inl a2 $-> inl a3
f, g: inl a1 $-> inl a2
p: f $-> g
cat_postcomp (inl a1) h f $->
cat_postcomp (inl a1) h 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
b1, b2, b3: B
h: inr b2 $-> inr b3
f, g: inr b1 $-> inr b2
p: f $-> g
cat_postcomp (inr b1) h f $->
cat_postcomp (inr b1) h g
    all: cbn in *; change (f $== g) in p; exact (h $@L 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
forall (a b c : A + B) 
(f : a $-> b), Is0Functor (cat_precomp c f) intros x y z h; 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
x, y, z: A + B
h: x $-> y
forall a b : y $-> z,
(a $-> b) -> cat_precomp z h a $-> cat_precomp z h b
    intros 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
x, y, z: A + B
h: x $-> y
f, g: y $-> z
p: f $-> g
cat_precomp z h f $-> cat_precomp z h g
    destruct x as [a1 | b1], y as [a2 | b2].
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, a2: A
z: A + B
h: inl a1 $-> inl a2
f, g: inl a2 $-> z
p: f $-> g
cat_precomp z h f $-> cat_precomp z h 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
a1: A
b2: B
z: A + B
h: inl a1 $-> inr b2
f, g: inr b2 $-> z
p: f $-> g
cat_precomp z h f $-> cat_precomp z h 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
b1: B
a2: A
z: A + B
h: inr b1 $-> inl a2
f, g: inl a2 $-> z
p: f $-> g
cat_precomp z h f $-> cat_precomp z h 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
b1, b2: B
z: A + B
h: inr b1 $-> inr b2
f, g: inr b2 $-> z
p: f $-> g
cat_precomp z h f $-> cat_precomp z h g
    2,3: contradiction.
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, a2: A
z: A + B
h: inl a1 $-> inl a2
f, g: inl a2 $-> z
p: f $-> g
cat_precomp z h f $-> cat_precomp z h 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
b1, b2: B
z: A + B
h: inr b1 $-> inr b2
f, g: inr b2 $-> z
p: f $-> g
cat_precomp z h f $-> cat_precomp z h g
    all: destruct z as [a3 | b3].
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, a2, a3: A
h: inl a1 $-> inl a2
f, g: inl a2 $-> inl a3
p: f $-> g
cat_precomp (inl a3) h f $-> cat_precomp (inl a3) h 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
a1, a2: A
b3: B
h: inl a1 $-> inl a2
f, g: inl a2 $-> inr b3
p: f $-> g
cat_precomp (inr b3) h f $-> cat_precomp (inr b3) h 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
b1, b2: B
a3: A
h: inr b1 $-> inr b2
f, g: inr b2 $-> inl a3
p: f $-> g
cat_precomp (inl a3) h f $-> cat_precomp (inl a3) h 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
b1, b2, b3: B
h: inr b1 $-> inr b2
f, g: inr b2 $-> inr b3
p: f $-> g
cat_precomp (inr b3) h f $-> cat_precomp (inr b3) h g
    2,3: contradiction.
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, a2, a3: A
h: inl a1 $-> inl a2
f, g: inl a2 $-> inl a3
p: f $-> g
cat_precomp (inl a3) h f $-> cat_precomp (inl a3) h 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
b1, b2, b3: B
h: inr b1 $-> inr b2
f, g: inr b2 $-> inr b3
p: f $-> g
cat_precomp (inr b3) h f $-> cat_precomp (inr b3) h g
    all: cbn in *; change (f $== g) in p; exact (p $@R h).
  -
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 | b1] [a2 | b2].
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, a2: A
forall (c d : A + B) (f : inl a1 $-> inl a2)
(g : inl a2 $-> 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
a1: A
b2: B
forall (c d : A + B) (f : inl a1 $-> inr b2)
(g : inr b2 $-> 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
b1: B
a2: A
forall (c d : A + B) (f : inr b1 $-> inl a2)
(g : inl a2 $-> 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
b1, b2: B
forall (c d : A + B) (f : inr b1 $-> inr b2)
(g : inr b2 $-> c) (h : c $-> d),
h $o g $o f $== h $o (g $o f)
    2,3: contradiction.
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, a2: A
forall (c d : A + B) (f : inl a1 $-> inl a2)
(g : inl a2 $-> 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
b1, b2: B
forall (c d : A + B) (f : inr b1 $-> inr b2)
(g : inr b2 $-> c) (h : c $-> d),
h $o g $o f $== h $o (g $o f)
    all: intros [a3 | b3].
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, a2, a3: A
forall (d : A + B) (f : inl a1 $-> inl a2)
(g : inl a2 $-> inl a3) 
(h : inl a3 $-> 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
a1, a2: A
b3: B
forall (d : A + B) (f : inl a1 $-> inl a2)
(g : inl a2 $-> inr b3) 
(h : inr b3 $-> 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
b1, b2: B
a3: A
forall (d : A + B) (f : inr b1 $-> inr b2)
(g : inr b2 $-> inl a3) 
(h : inl a3 $-> 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
b1, b2, b3: B
forall (d : A + B) (f : inr b1 $-> inr b2)
(g : inr b2 $-> inr b3) 
(h : inr b3 $-> d), h $o g $o f $== h $o (g $o f)
    2,3: contradiction.
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, a2, a3: A
forall (d : A + B) (f : inl a1 $-> inl a2)
(g : inl a2 $-> inl a3) 
(h : inl a3 $-> 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
b1, b2, b3: B
forall (d : A + B) (f : inr b1 $-> inr b2)
(g : inr b2 $-> inr b3) 
(h : inr b3 $-> d), h $o g $o f $== h $o (g $o f)
    all: intros [a4 | b4].
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, a2, a3, a4: A
forall (f : inl a1 $-> inl a2) 
(g : inl a2 $-> inl a3) 
(h : inl a3 $-> inl a4), 
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
a1, a2, a3: A
b4: B
forall (f : inl a1 $-> inl a2) 
(g : inl a2 $-> inl a3) 
(h : inl a3 $-> inr b4), 
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
b1, b2, b3: B
a4: A
forall (f : inr b1 $-> inr b2) 
(g : inr b2 $-> inr b3) 
(h : inr b3 $-> inl a4), 
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
b1, b2, b3, b4: B
forall (f : inr b1 $-> inr b2) 
(g : inr b2 $-> inr b3) 
(h : inr b3 $-> inr b4), 
h $o g $o f $== h $o (g $o f)
    2-3: contradiction.
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, a2, a3, a4: A
forall (f : inl a1 $-> inl a2) 
(g : inl a2 $-> inl a3) 
(h : inl a3 $-> inl a4), 
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
b1, b2, b3, b4: B
forall (f : inr b1 $-> inr b2) 
(g : inr b2 $-> inr b3) 
(h : inr b3 $-> inr b4), 
h $o g $o f $== h $o (g $o f)
    all: intros f g h; cbn; apply cat_assoc.
  -
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 | b1] [a2 | b2].
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, a2: A
forall (c d : A + B) (f : inl a1 $-> inl a2)
(g : inl a2 $-> 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
a1: A
b2: B
forall (c d : A + B) (f : inl a1 $-> inr b2)
(g : inr b2 $-> 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
b1: B
a2: A
forall (c d : A + B) (f : inr b1 $-> inl a2)
(g : inl a2 $-> 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
b1, b2: B
forall (c d : A + B) (f : inr b1 $-> inr b2)
(g : inr b2 $-> c) (h : c $-> d),
h $o (g $o f) $== h $o g $o f
    2,3: contradiction.
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, a2: A
forall (c d : A + B) (f : inl a1 $-> inl a2)
(g : inl a2 $-> 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
b1, b2: B
forall (c d : A + B) (f : inr b1 $-> inr b2)
(g : inr b2 $-> c) (h : c $-> d),
h $o (g $o f) $== h $o g $o f
    all: intros [a3 | b3].
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, a2, a3: A
forall (d : A + B) (f : inl a1 $-> inl a2)
(g : inl a2 $-> inl a3) 
(h : inl a3 $-> 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
a1, a2: A
b3: B
forall (d : A + B) (f : inl a1 $-> inl a2)
(g : inl a2 $-> inr b3) 
(h : inr b3 $-> 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
b1, b2: B
a3: A
forall (d : A + B) (f : inr b1 $-> inr b2)
(g : inr b2 $-> inl a3) 
(h : inl a3 $-> 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
b1, b2, b3: B
forall (d : A + B) (f : inr b1 $-> inr b2)
(g : inr b2 $-> inr b3) 
(h : inr b3 $-> d), h $o (g $o f) $== h $o g $o f
    2,3: contradiction.
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, a2, a3: A
forall (d : A + B) (f : inl a1 $-> inl a2)
(g : inl a2 $-> inl a3) 
(h : inl a3 $-> 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
b1, b2, b3: B
forall (d : A + B) (f : inr b1 $-> inr b2)
(g : inr b2 $-> inr b3) 
(h : inr b3 $-> d), h $o (g $o f) $== h $o g $o f
    all: intros [a4 | b4].
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, a2, a3, a4: A
forall (f : inl a1 $-> inl a2) 
(g : inl a2 $-> inl a3) 
(h : inl a3 $-> inl a4), 
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
a1, a2, a3: A
b4: B
forall (f : inl a1 $-> inl a2) 
(g : inl a2 $-> inl a3) 
(h : inl a3 $-> inr b4), 
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
b1, b2, b3: B
a4: A
forall (f : inr b1 $-> inr b2) 
(g : inr b2 $-> inr b3) 
(h : inr b3 $-> inl a4), 
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
b1, b2, b3, b4: B
forall (f : inr b1 $-> inr b2) 
(g : inr b2 $-> inr b3) 
(h : inr b3 $-> inr b4), 
h $o (g $o f) $== h $o g $o f
    2-3: contradiction.
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, a2, a3, a4: A
forall (f : inl a1 $-> inl a2) 
(g : inl a2 $-> inl a3) 
(h : inl a3 $-> inl a4), 
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
b1, b2, b3, b4: B
forall (f : inr b1 $-> inr b2) 
(g : inr b2 $-> inr b3) 
(h : inr b3 $-> inr b4), 
h $o (g $o f) $== h $o g $o f
    all: intros f g h; cbn; apply cat_assoc_opp.
  -
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 | b1] [a2 | b2] 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
a1, a2: A
f: inl a1 $-> inl a2
Id (inl a2) $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
a1: A
b2: B
f: inl a1 $-> inr b2
Id (inr b2) $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
b1: B
a2: A
f: inr b1 $-> inl a2
Id (inl a2) $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
b1, b2: B
f: inr b1 $-> inr b2
Id (inr b2) $o f $== f
    2, 3: contradiction.
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, a2: A
f: inl a1 $-> inl a2
Id (inl a2) $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
b1, b2: B
f: inr b1 $-> inr b2
Id (inr b2) $o f $== f
    all: cbn; apply 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 | b1] [a2 | b2] 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
a1, a2: A
f: inl a1 $-> inl a2
f $o Id (inl a1) $== 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
a1: A
b2: B
f: inl a1 $-> inr b2
f $o Id (inl a1) $== 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
b1: B
a2: A
f: inr b1 $-> inl a2
f $o Id (inr b1) $== 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
b1, b2: B
f: inr b1 $-> inr b2
f $o Id (inr b1) $== f
    2, 3: contradiction.
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, a2: A
f: inl a1 $-> inl a2
f $o Id (inl a1) $== 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
b1, b2: B
f: inr b1 $-> inr b2
f $o Id (inr b1) $== f
    all: cbn; apply cat_idr.
Defined.