proposition: Lemma eliminate_left_diagonal {x} : eliminate ⨂ id[x] ∘ ∆x ≈ unit_left⁻¹.
proof: Proof. apply (iso_to_monic unit_left). rewrite comp_assoc. rewrite unit_left_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