proposition: Corollary bimap_fmap {F : C ∏ D ⟶ E} {x w : C} {y z : D} (f : x ~{C}~> w) (g : y ~{D}~> z) : @fmap (C ∏ D) E F (x, y) (w, z) (f, g) = bimap f g.
proof: Proof. reflexivity. Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Construction.Product