{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. Proof. apply cat_coprod_rec. intros i. apply cat_prod_corec. intros a. destruct (dec_paths i a) as [p|]. - destruct p. exact (Id _). - apply zero_morphism. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans