{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.
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans