proposition: Lemma mempty_right_diagonal : mappend ∘ id ⨂ (mempty ∘ eliminate) ∘ ∆ grp ≈ id.
proof: Proof. rewrite bimap_comp_id_left. rewrite comp_assoc. rewrite mempty_right. apply proj_left_diagonal. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Naturality Category.Functor.Bifunctor Category.Structure.Monoidal.Proofs Category.Structure.Monoidal.Cartesian Category.Structure.Monoid Category.Structure.Group