Build_Is1Bifunctor'' {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C) `{!forall a, Is0Functor (F a), !forall b, Is0Functor (flip F b)} (Is0Bifunctor_F := Build_Is0Bifunctor'' F) `{!forall a, Is1Functor (F a), !forall b, Is1Functor (flip F b)} (bifunctor_coh : forall a0 a1 (f : a0 $-> a1) b0 b1 (g : b0 $-> b1), fmap01 F a1 g $o fmap10 F f b0 $== fmap10 F f b1 $o fmap01 F a0 g) : Is1Bifunctor F. Proof. snrapply Build_Is1Bifunctor. - exact _. - exact _. - exact _. - intros a0 a1 f b0 b1 g. exact (bifunctor_coh a0 a1 f b0 b1 g)^$. - reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics. Require Import Types.Forall Types.Prod. Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans