proposition: Lemma bimap_comp {F : C ∏ D ⟶ E} {x y z w u v} (f : y ~{C}~> z) (h : x ~{C}~> y) (g : v ~{D}~> w) (i : u ~{D}~> v) : bimap (f ∘ h) (g ∘ i) ≈ bimap f g ∘ bimap h i.
proof: Proof. unfold bimap. rewrite <- fmap_comp. apply fmap_respects. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Construction.Product