Build_Is0Bifunctor'' {A B C : Type} `{IsGraph A, IsGraph B, Is01Cat C} (F : A -> B -> C) `{!forall a, Is0Functor (F a), !forall b, Is0Functor (flip F b)} : Is0Bifunctor F. Proof. nrapply Build_Is0Bifunctor; exact _. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import Types.Forall Types.Prod. Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans