Build_Is1Bifunctor' {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A -> B -> C) `{!Is0Functor (uncurry F), !Is1Functor (uncurry F)} : Is1Bifunctor (Is0Bifunctor := Build_Is0Bifunctor' F) F. Proof. snrapply Build_Is1Bifunctor. - exact _. - exact (is1functor_functor_uncurried01 (uncurry F)). - exact (is1functor_functor_uncurried10 (uncurry F)). - intros a0 a1 f b0 b1 g. refine (_^$ $@ fmap_pair_comp (uncurry F) f (Id b0) (Id a1) g). exact (fmap2_pair (uncurry F) (cat_idl _) (cat_idr _)). - intros a0 a1 f b0 b1 g. refine (_^$ $@ fmap_pair_comp (uncurry F) (Id a0) g f (Id b1)). exact (fmap2_pair (uncurry F) (cat_idr _) (cat_idl _)). Defined.
Require Import Basics.Overture Basics.Tactics. Require Import Types.Forall Types.Prod. Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans