proposition: Lemma eliminate_right_diagonal {x} : id[x] ⨂ eliminate ∘ ∆x ≈ unit_right⁻¹.
proof: Proof. apply (iso_to_monic unit_right). rewrite comp_assoc. rewrite unit_right_eliminate. rewrite iso_to_from. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Bifunctor Category.Structure.Monoidal.Proofs Category.Structure.Monoidal.Cartesian