{A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A * B -> C) `{!forall a, Is0Functor (fun b => F (a,b)), !forall b, Is0Functor (fun a => F (a,b))} `{!forall a, Is1Functor (fun b => F (a,b)), !forall b, Is1Functor (fun a => F (a,b))} (bifunctor_coh : forall a0 a1 (f : a0 $-> a1) b0 b1 (g : b0 $-> b1), fmap (fun b => F (a1,b)) g $o fmap (fun a => F (a,b0)) f $== fmap (fun a => F(a,b1)) f $o fmap (fun b => F (a0,b)) g) : Is1Functor F. Proof. snrapply Build_Is1Functor. - intros [a b] [a' b'] [f g] [f' g'] [p p']; unfold fst, snd in * |- . exact (fmap2 (fun b0 => F (a,b0)) p' $@@ fmap2 (fun a0 => F (a0,b')) p). - intros [a b]. exact ((fmap_id (fun b0 => F (a,b0)) b $@@ fmap_id (fun a0 => F (a0,b)) _) $@ cat_idr _). - intros [a b] [a' b'] [a'' b''] [f g] [f' g']; unfold fst, snd in * |- . refine ((fmap_comp (fun b0 => F (a,b0)) g g' $@@ fmap_comp (fun a0 => F (a0,b'')) f f') $@ _). nrefine (cat_assoc_opp _ _ _ $@ (_ $@R _) $@ cat_assoc _ _ _). refine (cat_assoc _ _ _ $@ (_ $@L _^$) $@ cat_assoc_opp _ _ _). nrapply bifunctor_coh. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import Types.Prod.