proposition: Lemma tensor_id_left_inj {x y} (f g : x ~> y) : id[I] ⨂ f ≈ id[I] ⨂ g → f ≈ g.
proof: Proof. intros. rewrite <- id_right; symmetry; rewrite <- id_right; symmetry. rewrite <- (iso_to_from unit_left). rewrite !comp_assoc. rewrite !to_unit_left_natural. rewrites; reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Bifunctor Category.Structure.Monoidal