proposition: Lemma bimap_unit_right_id {x y z} : (id ⨂ unit_right) ⨂ id << (x ⨂ (y ⨂ I)) ⨂ z ~~> (x ⨂ y) ⨂ z >> unit_right ⨂ id ∘ tensor_assoc⁻¹ ⨂ id.
proof: Proof. pose proof (from_tensor_assoc_natural (id[x]) (@unit_right _ _ 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_from_to, id_right in X0. rewrites. rewrite comp_assoc; normal. pose proof (from_tensor_assoc_natural (id[x]) (id[y]) (@unit_left _ _ z)) as X0. rewrite bimap_id_id in X0. rewrite inverse_triangle_identity in X0. rewrite inverse_triangle_identity in X0. rewrite <- comp_assoc in X0. rewrite <- inverse_pentagon_identity in X0. rewrite !comp_assoc in X0. normal. symmetry in X0. rewrite bimap_comp_id_left in X0. rewrite comp_assoc in X0. assert (X2 : ∀ (f g : x ⨂ ((y ⨂ I) ⨂ z) ~{ C }~> (x ⨂ y) ⨂ z), f ∘ id ⨂ tensor_assoc⁻¹ ≈ g ∘ id ⨂ tensor_assoc⁻¹ → f ≈ g). { intros. assert (X3 : ∀ x y z w v (f g : x ⨂ (y ⨂ (z ⨂ v)) ~> w), f ≈ g → f ∘ (id[x] ⨂ tensor_assoc) ≈ g ∘ (id[x] ⨂ tensor_assoc)). { intros; rewrites; reflexivity. } apply X3 in X. normal. rewrite !iso_from_to in X. rewrite !bimap_id_id, !id_right in X. assumption. } apply X2 in X0; clear X2. rewrites. rewrite <- comp_assoc. rewrite iso_from_to, id_right. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Bifunctor Category.Structure.Monoidal