整数の定義を素朴なものに戻した。 --（succ (succ (pred zero))などが有効、という弱点がある） data Z : Set where zero : Z succ : Z -> Z pred : Z -> Z それに加法、反数、乗法を定義したものがこちら。 整数の素朴な定義この整数が環をなすことをAgda…