proposition: Theorem triangle_identity_left {x y} : unit_left ⨂ id << (I ⨂ x) ⨂ y ~~> x ⨂ y >> unit_left ∘ tensor_assoc.
proof: Proof. pose proof (@bimap_id_unit_left I x y). normal. apply tensor_id_left_inj in X. assumption. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Bifunctor Category.Structure.Monoidal