{A : Type} `{Is1Cat A} (x : A) `{!BinaryProduct x x} : x $-> cat_binprod x x. Proof. snrapply cat_binprod_corec; exact (Id _). Defined.
Require Import Basics.Equivalences Basics.Overture Basics.Tactics. Require Import Types.Bool Types.Prod Types.Forall. Require Import WildCat.Bifunctor WildCat.Core WildCat.Equiv WildCat.EquivGpd