Definition negpos : weq (coprod nat nat) ℤ. Proof. simple refine (make_weq _ (isweq_iso _ _ _ _)). { intros [n'|n]. { exact (natnattohz 0 (S n')). } { exact (natnattohz n 0). } } { intro i. destruct (hz_to_normal_form i) as [[n p]|[m q]]. { exact (inr n). } { exact (inl m). } } { intros [n'|n]. { simpl. rewrite natminuseqn. reflexivity. } { simpl. rewrite hzabsvalnat. reflexivity. } } { simpl. intro i. destruct (hz_to_normal_form i) as [[n p]|[m q]]. { exact p. } { exact q. } } Defined.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.