proposition: Lemma proj_right_tensor_id {x y z} : id ⨂ proj_right ≈ @proj_left _ _ _ x y ⨂ id[z] ∘ tensor_assoc⁻¹.
proof: Proof. unfold proj_left, proj_right. rewrite bimap_comp_id_left. rewrite inverse_triangle_identity. rewrite <- comp_assoc. rewrite <- from_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