{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. 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. 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). Proof. apply is0functor_op'. exact (is0functor_cat_prod I A^op). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans