proposition: Lemma proj_left_id_diagonal {x y} : proj_left ⨂ id ∘ ∆(x ⨂ y) ≈ tensor_assoc ∘ ∆x ⨂ id.
proof: Proof. rewrite diagonal_braid2. remember (_ ∘ _ ∘ tensor_assoc) as p. spose (@braid2_natural _ _ x _ id x _ id y _ eliminate y _ id) as X0. rewrite !bimap_id_id in X0. rewrite !id_left, !id_right in X0. unfold proj_left. normal. rewrite bimap_comp_id_right. rewrite <- !comp_assoc. rewrite (comp_assoc ((_ ⨂ _) ⨂ _)). unfold braid2 in X0. rewrite Heqp; clear Heqp p. rewrite X0; clear X0. normal. rewrite eliminate_left_diagonal. rewrite triangle_identity. rewrite <- !comp_assoc. rewrite (comp_assoc tensor_assoc). rewrite iso_to_from. normal. rewrite <- triangle_identity_left. normal. rewrite unit_left_braid. rewrite triangle_identity. rewrite <- !comp_assoc. rewrite iso_to_from. normal. rewrite to_tensor_assoc_natural. normal. rewrite iso_to_from. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Bifunctor Category.Structure.Monoidal.Proofs Category.Structure.Monoidal.Cartesian