proposition: Corollary unit_right_eliminate {x y} (f : x ~> y) : unit_right ∘ f ⨂ eliminate ∘ ∆x ≈ f.
proof: Proof. symmetry. rewrite <- id_left at 1. rewrite <- proj_left_diagonal. unfold proj_left. rewrite <- !comp_assoc. pose proof diagonal_natural; simpl in X. rewrite <- X; clear X. 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