{A B C : Type} (F : A -> B -> C) `{H : Is1Bifunctor A B C F} : Is1Bifunctor (flip F). Proof. snrapply Build_Is1Bifunctor. - change (Is1Functor (uncurry F o equiv_prod_symm _ _)). exact _. - exact _. - exact _. - intros b0 b1 g a0 a1 f. exact (fmap11_is_fmap10_fmap01 F f g). - intros b0 b1 g a0 a1 f. exact (fmap11_is_fmap01_fmap10 F f g). Defined.
Require Import Basics.Overture Basics.Tactics. Require Import Types.Forall Types.Prod. Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans