proposition: Theorem inverse_triangle_identity {x y} : id ⨂ unit_left << x ⨂ (I ⨂ y) ~~> x ⨂ y >> unit_right ⨂ id ∘ tensor_assoc⁻¹.
proof: Proof. rewrite triangle_identity. rewrite <- comp_assoc. rewrite iso_to_from; cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Bifunctor Category.Structure.Monoidal