{A B C : Type} `{IsGraph A, IsGraph B, Is01Cat C} (F : A * B -> C) `{!forall a, Is0Functor (fun b => F (a,b)), !forall b, Is0Functor (fun a => F (a,b))} : Is0Functor F. Proof. snrapply Build_Is0Functor. intros [a b] [a' b'] [f g]. exact (fmap (fun a0 => F (a0,b')) f $o fmap (fun b0 => F (a,b0)) g). Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import Types.Prod.