proposition: Lemma proj_left_tensor_id {x y z} : proj_left ⨂ id ≈ id[x] ⨂ @proj_right _ _ _ y z ∘ tensor_assoc.
proof: Proof. unfold proj_left, proj_right. rewrite bimap_comp_id_right. rewrite triangle_identity. rewrite <- comp_assoc. rewrite <- to_tensor_assoc_natural. normal; reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Bifunctor Category.Structure.Monoidal Category.Structure.Monoidal.Proofs Category.Structure.Monoidal.Semicartesian