proposition: Lemma bimap_id_unit_left {x y z} : id ⨂ (unit_left ⨂ id) << x ⨂ ((I ⨂ y) ⨂ z) ~~> x ⨂ (y ⨂ z) >> id ⨂ unit_left ∘ id ⨂ tensor_assoc.
proof: Proof. pose proof (to_tensor_assoc_natural (id[x]) (@unit_left _ _ y) (id[z])) as X0. assert (X1 : ∀ x y z w (f g : (x ⨂ y) ⨂ z ~> w), f ≈ g → f ∘ tensor_assoc⁻¹ ≈ g ∘ tensor_assoc⁻¹). { intros; rewrites; reflexivity. } apply X1 in X0. rewrite <- !comp_assoc in X0. rewrite iso_to_from, id_right in X0. rewrites. rewrite comp_assoc; normal. pose proof (to_tensor_assoc_natural (@unit_right _ _ x) (id[y]) (id[z])) as X0. rewrite bimap_id_id in X0. rewrite triangle_identity in X0. rewrite triangle_identity in X0. rewrite <- comp_assoc in X0. rewrite <- pentagon_identity in X0. rewrite !comp_assoc in X0. normal. symmetry in X0. rewrite bimap_comp_id_right in X0. rewrite comp_assoc in X0. assert (X2 : ∀ (f g : (x ⨂ I ⨂ y) ⨂ z ~{ C }~> x ⨂ y ⨂ z), f ∘ tensor_assoc ⨂ id ≈ g ∘ tensor_assoc ⨂ id → f ≈ g). { intros. assert (X3 : ∀ x y z w v (f g : ((x ⨂ y) ⨂ z) ⨂ v ~> w), f ≈ g → f ∘ (tensor_assoc⁻¹ ⨂ id[v]) ≈ g ∘ (tensor_assoc⁻¹ ⨂ id[v])). { intros; rewrites; reflexivity. } apply X3 in X. normal. rewrite !iso_to_from in X. rewrite !bimap_id_id, !id_right in X. assumption. } apply X2 in X0; clear X2. rewrites. rewrite <- comp_assoc. rewrite iso_to_from, id_right. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Bifunctor Category.Structure.Monoidal