proposition: Lemma cat_prod_pr_eta {z : A} {f f' : z $-> cat_prod x y} : cat_pr1 $o f $== cat_pr1 $o f' -> cat_pr2 $o f $== cat_pr2 $o f' -> f $== f'.
proof: Proof. intros fst snd. refine ((cat_prod_eta _)^$ $@ _ $@ cat_prod_eta _). by apply cat_prod_corec_eta. Defined.
imports: Basics EquivGpd Types.Prod WildCat.Core WildCat.ZeroGroupoid WildCat.Equiv WildCat.Yoneda WildCat.Universe WildCat.NatTrans WildCat.Opposite