proposition: Lemma proj_right_id_diagonal {x y} : proj_right ⨂ id ∘ ∆(x ⨂ y) ≈ tensor_assoc ∘ braid ⨂ id ∘ tensor_assoc⁻¹ ∘ id[x] ⨂ ∆y.
proof: Proof. rewrite diagonal_braid2. remember (_ ∘ _ ∘ tensor_assoc) as p. spose (@braid2_natural _ _ x _ eliminate x _ id y _ id y _ id) as X0. rewrite !bimap_id_id in X0. rewrite !id_right in X0. unfold braid2 in X0. unfold proj_right. normal. rewrite bimap_comp_id_right. rewrite <- !comp_assoc. rewrite (comp_assoc ((_ ⨂ _) ⨂ _)). rewrite Heqp; clear Heqp p. rewrite X0; clear X0. normal. rewrite eliminate_left_diagonal. rewrite triangle_identity_left. rewrite <- !comp_assoc. rewrite (comp_assoc tensor_assoc). rewrite iso_to_from. normal. rewrite <- to_unit_left_natural. rewrite <- !comp_assoc. repeat comp_left. rewrite comp_assoc. rewrite <- triangle_identity_left. 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