proposition: Lemma bimap_id_id {F : C ∏ D ⟶ E} {x y} : bimap (id[x]) (id[y]) ≈ id.
proof: Proof. destruct F; simpl. apply fmap_id. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Construction.Product