(x : Words) : amal_eta (x ++ word_inverse x) = mon_unit. Proof. induction x as [|x xs]. 1: reflexivity. destruct x as [h|k]. + cbn. rewrite app_assoc. 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 <- (app_nil (cons _ _)). change (amal_eta (([inl h] ++ [inl (- h)]) ++ nil) = mon_unit). rewrite <- app_assoc. 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 app_assoc. 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 <- (app_nil (cons _ _)). change (amal_eta (([inr k] ++ [inr (- k)]) ++ nil) = mon_unit). rewrite <- app_assoc. 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.
Require Import Basics Types. Require Import Cubical.DPath. Require Import Spaces.List.Core Spaces.List.Theory. Require Import Colimits.Pushout. Require Import Truncations.Core Truncations.SeparatedTrunc. Require Import Algebra.Groups.Group. Require Import WildCat.