proposition: Corollary unit_left_eliminate {x y} (f : x ~> y) : unit_left ∘ eliminate ⨂ f ∘ ∆x ≈ f.
proof: Proof. symmetry. rewrite <- id_left at 1. rewrite <- proj_right_diagonal. unfold proj_right. rewrite <- !comp_assoc. pose proof diagonal_natural as X0; simpl in X0. rewrite <- X0; clear X0. normal. rewrite eliminate_comp. 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