Coproducts.v

Require Import Basics.Overture Basics.Tactics Basics.Decidable.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Bool.
Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans
               WildCat.Opposite WildCat.Products WildCat.Universe
               WildCat.Yoneda WildCat.ZeroGroupoid WildCat.PointedCat
               WildCat.Monoidal.

(** * Categories with coproducts *)

Definition cat_coprod_rec_inv {I A : Type} `{Is1Cat A}
  (coprod : A) (x : I -> A) (z : A) (inj : forall i, x i $-> coprod)
  : yon_0gpd z coprod $-> prod_0gpd I (fun i => yon_0gpd z (x i))
  := cat_prod_corec_inv (coprod : A^op) x z inj.

Class Coproduct (I : Type) {A : Type} `{Is1Cat A} (x : I -> A)
  := prod_co_coprod :: Product (A:=A^op) I x.

Definition cat_coprod (I : Type) {A : Type} (x : I -> A) `{Coproduct I _ x} : A
  := cat_prod (A:=A^op) I x.

Definition cat_in {I : Type} {A : Type} {x : I -> A} `{Coproduct I _ x}
  : forall (i : I), x i $-> cat_coprod I x
  := cat_pr (A:=A^op) (x:=x).

Global Instance cat_isequiv_cat_coprod_rec_inv {I : Type} {A : Type}
  {x : I -> A} `{Coproduct I _ x}
  : forall (z : A), CatIsEquiv (cat_coprod_rec_inv (cat_coprod I x) x z cat_in)
  := cat_isequiv_cat_prod_corec_inv (A:=A^op) (x:=x).

(** A convenience wrapper for building coproducts *)
Definition Build_Coproduct (I : Type) {A : Type} `{Is1Cat A} {x : I -> A}
  (cat_coprod : A) (cat_in : forall i : I, x i $-> cat_coprod)
  (cat_coprod_rec : forall z : A,
    (forall i : I, x i $-> z) -> (cat_coprod $-> z))
  (cat_coprod_beta_in : forall (z : A) (f : forall i, x i $-> z) (i : I),
    cat_coprod_rec z f $o cat_in i $== f i)
  (cat_prod_eta_in : forall (z : A) (f g : cat_coprod $-> z),
    (forall i : I, f $o cat_in i $== g $o cat_in i) -> f $== g)
  : Coproduct I x
  := Build_Product I
      (cat_coprod : A^op)
      cat_in
      cat_coprod_rec
      cat_coprod_beta_in
      cat_prod_eta_in.

Section Lemmata.
  Context (I : Type) {A : Type} {x : I -> A} `{Coproduct I _ x}.

  Definition cate_cat_coprod_rec_inv {z : A}
    : yon_0gpd z (cat_coprod I x) $<~> prod_0gpd I (fun i => yon_0gpd z (x i))
    := cate_cat_prod_corec_inv I (A:=A^op) (x:=x).

  Definition cate_cate_coprod_rec {z : A}
    : prod_0gpd I (fun i => yon_0gpd z (x i)) $<~> yon_0gpd z (cat_coprod I x)
    := cate_cat_prod_corec I (A:=A^op) (x:=x).

  Definition cat_coprod_rec {z : A}
    : (forall i, x i $-> z) -> cat_coprod I x $-> z
    := cat_prod_corec I (A:=A^op) (x:=x).

  Definition cat_coprod_beta {z : A} (f : forall i, x i $-> z)
    : forall i, cat_coprod_rec f $o cat_in i $== f i
    := cat_prod_beta I (A:=A^op) (x:=x) f.

  Definition cat_coprod_eta {z : A} (f : cat_coprod I x $-> z)
    : cat_coprod_rec (fun i => f $o cat_in i) $== f
    := cat_prod_eta I (A:=A^op) (x:=x) f.

  Definition natequiv_cat_coprod_rec_inv
    : NatEquiv (fun z => yon_0gpd z (cat_coprod I x))
      (fun z : A => prod_0gpd I (fun i => yon_0gpd z (x i)))
    := natequiv_cat_prod_corec_inv I (A:=A^op) (x:=x).

  Definition cat_coprod_rec_eta {z : A} {f g : forall i, x i $-> z}
    : (forall i, f i $== g i) -> cat_coprod_rec f $== cat_coprod_rec g
    := cat_prod_corec_eta I (A:=A^op) (x:=x).

  Definition cat_coprod_in_eta {z : A} {f g : cat_coprod I x $-> z}
    : (forall i, f $o cat_in i $== g $o cat_in i) -> f $== g
    := cat_prod_pr_eta I (A:=A^op) (x:=x).
End Lemmata.

(** *** Codiagonal / fold map *)

Definition cat_coprod_fold {I : Type} {A : Type} (x : A) `{Coproduct I _ (fun _ => x)}
  : cat_coprod I (fun _ => x) $-> x
  := cat_prod_diag (A:=A^op) x.

(** *** Uniqueness of coproducts *)

(** [I]-indexed coproducts are unique no matter how they are constructed. *)
Definition cate_cat_coprod {I J : Type} (ie : I <~> J) {A : Type} `{HasEquivs A}
  (x : I -> A) `{!Coproduct I x} (y : J -> A) `{!Coproduct J y}
  (e : forall (i : I), y (ie i) $<~> x i)
  : cat_coprod J y $<~> cat_coprod I x
  := cate_cat_prod (A:=A^op) ie x y e.

(** *** Existence of coproducts *)

Class HasCoproducts (I A : Type) `{Is1Cat A}
  := has_coproducts :: forall x : I -> A, Coproduct I x.

Class HasAllCoproducts (A : Type) `{Is1Cat A}
  := has_all_coproducts :: forall I : Type, HasCoproducts I A.

(** *** Coproduct functor *)

Local Instance hasproductsop_hascoproducts {I A : Type} `{HasCoproducts I A}
  : HasProducts I A^op
  := fun x : I -> A^op => @has_coproducts I A _ _ _ _ _ x.

Global Instance is0functor_cat_coprod (I : Type) `{IsGraph I}
  (A : Type) `{HasCoproducts I A}
  : @Is0Functor (I -> A) A (isgraph_forall I (fun _ => A)) _
    (fun x : I -> A => cat_coprod I x).I: Type
H: IsGraph I
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
H1: HasCoproducts I A
Is0Functor (fun x : I -> A => cat_coprod I x)
Proof.I: Type
H: IsGraph I
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
H1: HasCoproducts I A
Is0Functor (fun x : I -> A => cat_coprod I x)
  apply is0functor_op'.I: Type
H: IsGraph I
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
H1: HasCoproducts I A
Is0Functor (fun x : I -> A => cat_coprod I x)
  exact (is0functor_cat_prod I A^op).
Defined.

Global Instance is1functor_cat_coprod (I : Type) `{IsGraph I}
  (A : Type) `{HasCoproducts I A}
  : @Is1Functor (I -> A) A _ _ _ (is1cat_forall I (fun _ => A)) _ _ _ _
    (fun x : I -> A => cat_coprod I x) _.I: Type
H: IsGraph I
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
H1: HasCoproducts I A
Is1Functor (fun x : I -> A => cat_coprod I x)
Proof.I: Type
H: IsGraph I
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
H1: HasCoproducts I A
Is1Functor (fun x : I -> A => cat_coprod I x)
  apply is1functor_op'.I: Type
H: IsGraph I
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
H1: HasCoproducts I A
Is1Functor (fun x : I -> A => cat_coprod I x)
  exact (is1functor_cat_prod I A^op).
Defined.

(** *** Categories with specific kinds of coproducts *)

Definition isinitial_coprodempty {A : Type} {z : A}
  `{Coproduct Empty A (fun _ => z)}
  : IsInitial (cat_coprod Empty (fun _ => z)).A: Type
z: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: Coproduct Empty (fun _ : Empty => z)
IsInitial (cat_coprod Empty (fun _ : Empty => z))
Proof.A: Type
z: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: Coproduct Empty (fun _ : Empty => z)
IsInitial (cat_coprod Empty (fun _ : Empty => z))
  intros a.A: Type
z: A
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: Coproduct Empty (fun _ : Empty => z)
a: A
{f : cat_coprod Empty (fun _ : Empty => z) $-> a &
forall
g : cat_coprod Empty (fun _ : Empty => z) $-> a,
f $== g}
  snrefine (cat_coprod_rec _ _; fun f => cat_coprod_in_eta _ _); intros [].
Defined.

(** *** Binary coproducts *)

Class BinaryCoproduct {A : Type} `{Is1Cat A} (x y : A)
  := prod_co_bincoprod :: BinaryProduct (x : A^op) (y : A^op).

Definition cat_bincoprod {A : Type}  `{Is1Cat  A} (x y : A) `{!BinaryCoproduct x y} : A
  := cat_binprod (x : A^op) y.

Definition cat_inl {A : Type} `{Is1Cat A} {x y : A} `{!BinaryCoproduct x y}
  : x $-> cat_bincoprod x y
  := cat_pr1 (A:=A^op) (x:=x) (y:=y).

Definition cat_inr {A : Type} `{Is1Cat A} {x y : A} `{!BinaryCoproduct x y}
  : y $-> cat_bincoprod x y
  := cat_pr2 (A:=A^op) (x:=x) (y:=y).

(** A category with binary coproducts is a category with a binary coproduct for each pair of objects. *)
Class HasBinaryCoproducts (A : Type) `{Is1Cat A}
  := binary_coproducts :: forall x y, BinaryCoproduct x y.

Global Instance hasbinarycoproducts_hascoproductsbool {A : Type}
  `{HasCoproducts Bool A}
  : HasBinaryCoproducts A
  := fun x y => has_coproducts (fun b : Bool => if b then x else y).

(** A convenience wrapper for building binary coproducts *)
Definition Build_BinaryCoproduct {A : Type} `{Is1Cat A} {x y : A}
  (cat_coprod : A) (cat_inl : x $-> cat_coprod) (cat_inr : y $-> cat_coprod)
  (cat_coprod_rec : forall z : A, (x $-> z) -> (y $-> z) -> cat_coprod $-> z)
  (cat_coprod_beta_inl : forall (z : A) (f : x $-> z) (g : y $-> z),
    cat_coprod_rec z f g $o cat_inl $== f)
  (cat_coprod_beta_inr : forall (z : A) (f : x $-> z) (g : y $-> z),
    cat_coprod_rec z f g $o cat_inr $== g)
  (cat_coprod_in_eta : forall (z : A) (f g : cat_coprod $-> z),
    f $o cat_inl $== g $o cat_inl -> f $o cat_inr $== g $o cat_inr -> f $== g)
  : BinaryCoproduct x y
  := Build_BinaryProduct
      (cat_coprod : A^op)
      cat_inl
      cat_inr
      cat_coprod_rec
      cat_coprod_beta_inl
      cat_coprod_beta_inr
      cat_coprod_in_eta.

Section Lemmata.
  Context {A : Type} {x y z : A} `{BinaryCoproduct _ x y}.

  Definition cat_bincoprod_rec (f : x $-> z) (g : y $-> z)
    : cat_bincoprod x y $-> z
    := @cat_binprod_corec A^op _ _ _ _ x y _ _ f g.

  Definition cat_bincoprod_beta_inl (f : x $-> z) (g : y $-> z)
    : cat_bincoprod_rec f g $o cat_inl $== f
    := @cat_binprod_beta_pr1 A^op _ _ _ _ x y _ _ f g.

  Definition cat_bincoprod_beta_inr (f : x $-> z) (g : y $-> z)
    : cat_bincoprod_rec f g $o cat_inr $== g
    := @cat_binprod_beta_pr2 A^op _ _ _ _ x y _ _ f g.

  Definition cat_bincoprod_eta (f : cat_bincoprod x y $-> z)
    : cat_bincoprod_rec (f $o cat_inl) (f $o cat_inr) $== f
    := @cat_binprod_eta A^op _ _ _ _ x y _ _ f.

  Definition cat_bincoprod_eta_in {f g : cat_bincoprod x y $-> z}
    : f $o cat_inl $== g $o cat_inl -> f $o cat_inr $== g $o cat_inr -> f $== g
    := @cat_binprod_eta_pr A^op _ _ _ _ x y _ _ f g.

  Definition cat_bincoprod_rec_eta {f f' : x $-> z} {g g' : y $-> z}
    : f $== f' -> g $== g' -> cat_bincoprod_rec f g $== cat_bincoprod_rec f' g'
    := @cat_binprod_corec_eta A^op _ _ _ _ x y _ _ f f' g g'.
End Lemmata.

(** *** Symmetry of coproducts *)

Definition cate_bincoprod_swap {A : Type} `{HasEquivs A}
  {e : HasBinaryCoproducts A} (x y : A)
  : cat_bincoprod x y $<~> cat_bincoprod y x.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
e: HasBinaryCoproducts A
x, y: A
cat_bincoprod x y $<~> cat_bincoprod y x
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
e: HasBinaryCoproducts A
x, y: A
cat_bincoprod x y $<~> cat_bincoprod y x
  exact (@cate_binprod_swap A^op _ _ _ _ _ e _ _).
Defined.

(** *** Associativity of coproducts *)

Lemma cate_coprod_assoc {A : Type} `{HasEquivs A}
  {e : HasBinaryCoproducts A} (x y z : A)
  : cat_bincoprod x (cat_bincoprod y z)
    $<~> cat_bincoprod (cat_bincoprod x y) z.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
e: HasBinaryCoproducts A
x, y, z: A
cat_bincoprod x (cat_bincoprod y z) $<~>
cat_bincoprod (cat_bincoprod x y) z
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasEquivs A
e: HasBinaryCoproducts A
x, y, z: A
cat_bincoprod x (cat_bincoprod y z) $<~>
cat_bincoprod (cat_bincoprod x y) z
  exact (@associator_binprod A^op _ _ _ _ _ e x y z)^-1$.
Defined.

(** *** Binary coproduct functor *)

(** Hint: Use [Set Printing Implicit] to see the implicit arguments in the following proofs. *)

Global Instance is0functor_cat_bincoprod_l {A : Type}
  `{H0 : HasBinaryCoproducts A} y
  : Is0Functor (A:=A) (fun x => cat_bincoprod x y).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasBinaryCoproducts A
y: A
Is0Functor (fun x : A => cat_bincoprod x y)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasBinaryCoproducts A
y: A
Is0Functor (fun x : A => cat_bincoprod x y)
  rapply is0functor_op'.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasBinaryCoproducts A
y: A
Is0Functor (fun x : A => cat_bincoprod x y)
  exact (is0functor_cat_binprod_l (A:=A^op) (H0:=H0) y).
Defined.

Global Instance is1functor_cat_bincoprod_l {A : Type}
  `{H0 : HasBinaryCoproducts A} y
  : Is1Functor (fun x => cat_bincoprod x y).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasBinaryCoproducts A
y: A
Is1Functor (fun x : A => cat_bincoprod x y)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasBinaryCoproducts A
y: A
Is1Functor (fun x : A => cat_bincoprod x y)
  rapply is1functor_op'.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasBinaryCoproducts A
y: A
Is1Functor (fun x : A => cat_bincoprod x y)
  exact (is1functor_cat_binprod_l (A:=A^op) (H0:=H0) y).
Defined.

Global Instance is0functor_cat_bincoprod_r {A : Type}
  `{H0 : HasBinaryCoproducts A} x
  : Is0Functor (fun y => cat_bincoprod x y).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasBinaryCoproducts A
x: A
Is0Functor (fun y : A => cat_bincoprod x y)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasBinaryCoproducts A
x: A
Is0Functor (fun y : A => cat_bincoprod x y)
  rapply is0functor_op'.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasBinaryCoproducts A
x: A
Is0Functor (fun y : A => cat_bincoprod x y)
  exact (is0functor_cat_binprod_r (A:=A^op) (H0:=H0) x).
Defined.

Global Instance is1functor_cat_bincoprod_r {A : Type}
  `{H0 : HasBinaryCoproducts A} x
  : Is1Functor (fun y => cat_bincoprod x y).A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasBinaryCoproducts A
x: A
Is1Functor (fun y : A => cat_bincoprod x y)
Proof.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasBinaryCoproducts A
x: A
Is1Functor (fun y : A => cat_bincoprod x y)
  rapply is1functor_op'.A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H: Is1Cat A
H0: HasBinaryCoproducts A
x: A
Is1Functor (fun y : A => cat_bincoprod x y)
  exact (is1functor_cat_binprod_r (A:=A^op) (H0:=H0) x).
Defined.

(** *** Coproducts in Type *)

(** [Type] has all coproducts. *)
Global Instance hasallcoproducts_type : HasAllCoproducts Type.HasAllCoproducts Type
Proof.HasAllCoproducts Type
  intros I x.I: Type
x: I -> Type
Coproduct I x
  snrapply Build_Coproduct.I: Type
x: I -> Type
Type
I: Type
x: I -> Type
forall i : I, x i $-> ?cat_coprod
I: Type
x: I -> Type
forall z : Type,
(forall i : I, x i $-> z) -> ?cat_coprod $-> z
I: Type
x: I -> Type
forall (z : Type) (f : forall i : I, x i $-> z)
(i : I), ?cat_coprod_rec z f $o ?cat_in i $== f i
I: Type
x: I -> Type
forall (z : Type) (f g : ?cat_coprod $-> z),
(forall i : I, f $o ?cat_in i $== g $o ?cat_in i) ->
f $== g
  -I: Type
x: I -> Type
Type exact (sig (fun i : I => x i)).
  -I: Type
x: I -> Type
forall i : I, x i $-> {i0 : I & x i0} exact (exist x).
  -I: Type
x: I -> Type
forall z : Type,
(forall i : I, x i $-> z) -> {i : I & x i} $-> z intros A f [i xi].I: Type
x: I -> Type
A: Type
f: forall i : I, x i $-> A
i: I
xi: x i
A
    exact (f i xi).
  -I: Type
x: I -> Type
forall (z : Type) (f : forall i : I, x i $-> z)
(i : I),
(fun (A : Type) (f0 : forall i0 : I, x i0 $-> A) =>
 (fun X : {i0 : I & x i0} =>
  (fun (i0 : I) (xi : x i0) => f0 i0 xi) X.1 X.2)
 :
 {i0 : I & x i0} $-> A) z f $o exist x i $== f i intros A f i xi; reflexivity.
  -I: Type
x: I -> Type
forall (z : Type) (f g : {i : I & x i} $-> z),
(forall i : I, f $o exist x i $== g $o exist x i) ->
f $== g intros A f g p [i xi].I: Type
x: I -> Type
A: Type
f, g: {i : I & x i} $-> A
p: forall i : I, f $o exist x i $== g $o exist x i
i: I
xi: x i
f (i; xi) = g (i; xi)
    exact (p i xi).
Defined.

(** In particular, [Type] has all binary coproducts. *)
Global Instance hasbinarycoproducts_type : HasBinaryCoproducts Type
  := {}.

(** ** Canonical coproduct-product map *)

(** There is a canonical map from a coproduct to a product when the indexing set has decidable equality and the category is pointed. *)
Definition cat_coprod_prod {I : Type} `{DecidablePaths I} {A : Type}
  `{Is1Cat A, !IsPointedCat A}
  (x : I -> A) `{!Coproduct I x, !Product I x}
  : cat_coprod I x $-> cat_prod I x.I: Type
H: DecidablePaths I
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsPointedCat0: IsPointedCat A
x: I -> A
Coproduct0: Coproduct I x
Product0: Product I x
cat_coprod I x $-> cat_prod I x 
Proof.I: Type
H: DecidablePaths I
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsPointedCat0: IsPointedCat A
x: I -> A
Coproduct0: Coproduct I x
Product0: Product I x
cat_coprod I x $-> cat_prod I x
  apply cat_coprod_rec.I: Type
H: DecidablePaths I
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsPointedCat0: IsPointedCat A
x: I -> A
Coproduct0: Coproduct I x
Product0: Product I x
forall i : I, x i $-> cat_prod I x
  intros i.I: Type
H: DecidablePaths I
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsPointedCat0: IsPointedCat A
x: I -> A
Coproduct0: Coproduct I x
Product0: Product I x
i: I
x i $-> cat_prod I x
  apply cat_prod_corec.I: Type
H: DecidablePaths I
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsPointedCat0: IsPointedCat A
x: I -> A
Coproduct0: Coproduct I x
Product0: Product I x
i: I
forall i0 : I, x i $-> x i0
  intros a.I: Type
H: DecidablePaths I
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsPointedCat0: IsPointedCat A
x: I -> A
Coproduct0: Coproduct I x
Product0: Product I x
i, a: I
x i $-> x a
  destruct (dec_paths i a) as [p|].I: Type
H: DecidablePaths I
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsPointedCat0: IsPointedCat A
x: I -> A
Coproduct0: Coproduct I x
Product0: Product I x
i, a: I
p: i = a
x i $-> x a
I: Type
H: DecidablePaths I
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsPointedCat0: IsPointedCat A
x: I -> A
Coproduct0: Coproduct I x
Product0: Product I x
i, a: I
n: i <> a
x i $-> x a
  -I: Type
H: DecidablePaths I
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsPointedCat0: IsPointedCat A
x: I -> A
Coproduct0: Coproduct I x
Product0: Product I x
i, a: I
p: i = a
x i $-> x a destruct p.I: Type
H: DecidablePaths I
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsPointedCat0: IsPointedCat A
x: I -> A
Coproduct0: Coproduct I x
Product0: Product I x
i: I
x i $-> x i
    exact (Id _).
  -I: Type
H: DecidablePaths I
A: Type
IsGraph0: IsGraph A
Is2Graph0: Is2Graph A
Is01Cat0: Is01Cat A
H0: Is1Cat A
IsPointedCat0: IsPointedCat A
x: I -> A
Coproduct0: Coproduct I x
Product0: Product I x
i, a: I
n: i <> a
x i $-> x a apply zero_morphism. 
Defined.