proposition: Lemma amal_eta_word_concat_wV (x : Words) : amal_eta (x ++ word_inverse x) = mon_unit.
proof: Proof. induction x as [|x xs]. 1: reflexivity. destruct x as [h|k]. + cbn. rewrite word_concat_w_ww. change (amal_eta ([inl h]) * amal_eta ((xs ++ word_inverse xs)) * amal_eta ([inl (- h)]) = mon_unit). rewrite IHxs. rewrite rightidentity_sgop_amal_type. rewrite <- (word_concat_w_nil (cons _ _)). change (amal_eta (([inl h] ++ [inl (- h)]) ++ nil) = mon_unit). rewrite <- word_concat_w_ww. change (amal_eta (nil ++ [inl h] ++ [inl (- h)] ++ nil) = mon_unit). refine (amal_mu_H _ _ _ _ @ _). refine (_ @ _). { apply ap, ap. rapply (ap (fun x => x ++ _)). rapply (ap (fun x => [x])). apply ap. apply right_inverse. } apply amal_omega_H. + cbn. rewrite word_concat_w_ww. change (amal_eta ([inr k]) * amal_eta ((xs ++ word_inverse xs)) * amal_eta ([inr (-k)]) = mon_unit). rewrite IHxs. rewrite rightidentity_sgop_amal_type. rewrite <- (word_concat_w_nil (cons _ _)). change (amal_eta (([inr k] ++ [inr (- k)]) ++ nil) = mon_unit). rewrite <- word_concat_w_ww. change (amal_eta (nil ++ [inr k] ++ [inr (- k)] ++ nil) = mon_unit). refine (amal_mu_K _ _ _ _ @ _). refine (_ @ _). { apply ap, ap. rapply (ap (fun x => x ++ _)). rapply (ap (fun x => [x])). apply ap. apply right_inverse. } apply amal_omega_K. Defined.
imports: Basics Types Cubical Spaces.List Colimits.Pushout Truncations.Core Truncations.SeparatedTrunc Algebra.Groups.Group WildCat