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