proposition: Lemma cat_prod_corec_eta {z : A} {f f' : z $-> x} {g g' : z $-> y} : f $== f' -> g $== g' -> cat_prod_corec f g $== cat_prod_corec f' g'.
proof: Proof. intros p q. unfold cat_prod_corec. apply (moveL_equiv_V_0gpd cate_cat_prod_corec_inv). refine (cate_isretr cate_cat_prod_corec_inv _ $@ _). split. - exact p. - exact q. Defined.
imports: Basics EquivGpd Types.Prod WildCat.Core WildCat.ZeroGroupoid WildCat.Equiv WildCat.Yoneda WildCat.Universe WildCat.NatTrans WildCat.Opposite