proposition: Lemma mappend_inverse : mappend ∘ inverse[grp] ⨂ inverse[grp] ≈ inverse[grp] ∘ mappend ∘ braid.
proof: Proof. rewrite <- (comp_assoc inverse[grp] mappend braid). apply left_inverse_unique. rewrite bimap_comp. rewrite <- bimap_id_right_left. rewrite !comp_assoc. rewrite mappend_assoc. rewrite <- bimap_id_id. rewrite <- (comp_assoc _ tensor_assoc _). rewrite <- to_tensor_assoc_natural. rewrite comp_assoc; rewrite <- (comp_assoc _ (id ⨂ mappend) _). rewrite <- bimap_comp; rewrite id_left. rewrite mappend_assoc_sym. rewrite <- (comp_assoc _ tensor_assoc _). rewrite <- to_tensor_assoc_natural. rewrite !comp_assoc; rewrite <- (comp_assoc mappend _ _). rewrite <- bimap_comp; rewrite id_left. rewrite diagonal_braid2. rewrite !comp_assoc; rewrite <- (comp_assoc _ tensor_assoc (tensor_assoc ⁻¹)). rewrite iso_to_from; rewrite id_right. rewrite <- (comp_assoc _ (inverse[grp] ⨂ _) _). rewrite <- bimap_comp; rewrite id_right. rewrite hexagon_rotated. rewrite !comp_assoc; rewrite <- (comp_assoc _ (inverse[grp] ⨂ braid) _). rewrite <- bimap_comp; rewrite id_right. rewrite braid_invol. rewrite <- bimap_id_id. rewrite <- (comp_assoc _ (tensor_assoc ⁻¹) _). rewrite <- from_tensor_assoc_natural. rewrite !comp_assoc; rewrite <- (comp_assoc _ (tensor_assoc ⁻¹) _). rewrite iso_from_to; rewrite id_right. rewrite <- (bimap_id_left_right ∆grp ∆grp). rewrite !comp_assoc; rewrite <- (comp_assoc _ tensor_assoc _). rewrite <- bimap_id_id. rewrite <- to_tensor_assoc_natural. rewrite !comp_assoc; rewrite <- (comp_assoc mappend (inverse[grp] ⨂ _) _). rewrite <- bimap_comp; rewrite id_right. rewrite <- (comp_assoc _ braid _). rewrite <- bimap_braid. rewrite !comp_assoc; rewrite <- (comp_assoc _ ((inverse[grp] ⨂ id) ⨂ id) _). rewrite <- bimap_comp; rewrite id_left. rewrite <- (comp_assoc _ (mappend ⨂ id) _). rewrite <- bimap_comp; rewrite id_left. rewrite !comp_assoc. rewrite left_inverse. rewrite bimap_comp_id_right. rewrite !comp_assoc. rewrite mempty_left. rewrite <- (comp_assoc _ (eliminate ⨂ id) braid). rewrite bimap_braid. rewrite comp_assoc. rewrite unit_left_braid. rewrite <- (id_left inverse[grp]). rewrite bimap_comp. rewrite comp_assoc; rewrite <- (comp_assoc _ _ tensor_assoc). rewrite to_tensor_assoc_natural. rewrite comp_assoc. rewrite triangle_identity_right. rewrite comp_assoc; rewrite <- (comp_assoc _ _ tensor_assoc). rewrite iso_from_to; rewrite id_right. rewrite <- (comp_assoc _ _ (∆grp ⨂ id[grp])). rewrite <- bimap_comp; rewrite id_right. rewrite <- bimap_id_right_left. rewrite !comp_assoc. rewrite <- (comp_assoc _ unit_right _). rewrite <- to_unit_right_natural. rewrite !comp_assoc. rewrite left_inverse. rewrite <- !comp_assoc. rewrite eliminate_comp. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Naturality Category.Functor.Bifunctor Category.Structure.Monoidal.Proofs Category.Structure.Monoidal.Cartesian Category.Structure.Monoid Category.Structure.Group