proposition: Lemma bimap_comp_id_right {F : C ∏ D ⟶ E} {w} `(f : y ~{C}~> z) `(g : x ~{C}~> y) : bimap (f ∘ g) (id[w]) ≈ bimap f id ∘ bimap g id.
proof: Proof. unfold bimap. rewrite <- fmap_comp. apply fmap_respects. split; simpl; cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Construction.Product