Definition negpos' : isweq (@pr1 _ hz_normal_form). Proof. apply isweqpr1; intro i. exists (hz_to_normal_form i). generalize (hz_to_normal_form i) as s. intros [[m p]|[m p]] [[n q]|[n q]]. { apply (maponpaths (@ii1 (∑ n, natnattohz n 0 = i) (∑ n, natnattohz 0 (S n) = i))). apply (proofirrelevance _ (isinclnattohz i)). } { apply fromempty. assert (r := p@!q); clear p q. apply (hzdichot r). } { apply fromempty. assert (r := q@!p); clear p q. apply (hzdichot r). } { apply (maponpaths (@ii2 (∑ n, natnattohz n 0 = i) (∑ n, natnattohz 0 (S n) = i))). assert (p' := maponpaths hzsign p). assert (q' := maponpaths hzsign q). change (- natnattohz O (S m)) with (nattohz (S m)) in p'. change (- natnattohz O (S n)) with (nattohz (S n)) in q'. assert (c := proofirrelevance _ (isinclnattohz (-i)) (S m,,p') (S n,,q')). assert (d := maponpaths pr1 c); simpl in d. assert (e := invmaponpathsS _ _ d); clear d. apply subtypePath. - intro; apply setproperty. - exact (!e). } Defined.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.