{A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C} (F : A * B -> C) `{!Is0Functor F, !Is1Functor F} {a0 a1 : A} {f f' : a0 $-> a1} (p : f $== f') {b0 b1 : B} {g g' : b0 $-> b1} (q : g $== g') : fmap_pair F f g $== fmap_pair F f' g' := fmap2 F (a := (a0, b0)) (b := (a1, b1)) (f := (f, g)) (g := (f' ,g')) (p, q).
Require Import Basics.Overture Basics.Tactics. Require Import WildCat.Core. Require Import WildCat.Equiv. Require Import Types.Prod.