{A B C : Type} `{HasEquivs A, HasEquivs B, HasEquivs C} (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F} {a0 a1 : A} (f : a0 $<~> a1) {b0 b1 : B} (g : b0 $<~> b1) : F a0 b0 $<~> F a1 b1 := Build_CatEquiv (fmap11 F f g).
Require Import Basics.Overture Basics.Tactics. Require Import Types.Forall Types.Prod. Require Import WildCat.Core WildCat.Prod WildCat.Equiv WildCat.NatTrans