proposition: Theorem inverse_pentagon_identity {x y z w} : tensor_assoc⁻¹ ⨂ id[w] ∘ tensor_assoc⁻¹ ∘ id[x] ⨂ tensor_assoc⁻¹ << x ⨂ (y ⨂ (z ⨂ w)) ~~> ((x ⨂ y) ⨂ z) ⨂ w >> tensor_assoc⁻¹ ∘ tensor_assoc⁻¹.
proof: Proof. apply (iso_to_epic tensor_assoc). rewrite <- !comp_assoc. rewrite iso_from_to, id_right. apply (iso_to_epic tensor_assoc). rewrite iso_from_to. rewrite <- !comp_assoc. rewrite <- pentagon_identity. normal. rewrite iso_from_to; normal. rewrite <- !comp_assoc. rewrite (comp_assoc (tensor_assoc⁻¹)). rewrite iso_from_to; normal. rewrite iso_from_to; normal. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Bifunctor Category.Structure.Monoidal