proposition: Theorem bimap_triangle_left {x y} : unit_left << I ⨂ (x ⨂ y) ~~> x ⨂ y >> bimap unit_left id ∘ tensor_assoc⁻¹.
proof: Proof. rewrite triangle_identity_left. 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