{A B C : Type} (F : A -> B -> C) `{Is01Cat A, Is01Cat B, Is01Cat C, !Is0Bifunctor F} : Is0Bifunctor (flip F). Proof. snrapply Build_Is0Bifunctor. - change (Is0Functor (uncurry F o equiv_prod_symm _ _)). exact _. - exact _. - exact _. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import Types.Forall Types.Prod. Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans