Contents

The modulus relation

The basic relation in modular arithmetic is the modulus relation. In dependent type theory with a natural numbers type and function types, one could define the modulus relation on the natural numbers as a ternary inductive type family $m \equiv n \mod k$ indexed by natural numbers $m:\mathbb{N}$, $n:\mathbb{N}$, and $k:\mathbb{N}$, inductively defined by the following constructors:

• for each $k:\mathbb{N}$, a term
$\mathrm{indzero}(k):0 \equiv 0 \mod k$
• for each $k:\mathbb{N}$, $m:\mathbb{N}$ and $n:\mathbb{N}$, a function
$\mathrm{indsucc}(m, n, k):(m \equiv n \mod k) \to (s(m) \equiv s(n) \mod k)$
• for each $k:\mathbb{N}$, $m:\mathbb{N}$ and $n:\mathbb{N}$, a term
$\mathrm{indmodleft}(m, n, k):m \cdot k \equiv 0 \mod k$
• for each $k:\mathbb{N}$, $m:\mathbb{N}$ and $n:\mathbb{N}$, a term
$\mathrm{indmodright}(m, n, k):0 \equiv n \cdot k \mod k$

where $m \cdot n$ is multiplication of two natural numbers $m:\mathbb{N}$ and $n:\mathbb{N}$.

For each nonzero natural number $k$, the type $(\mathbb{N}, m \equiv n \mod k)$ is equivalent to the finite type $\mathrm{Fin}(k)$ equipped with its canonical identity type. When $k$ is zero the type $(\mathbb{N}, m \equiv n \mod k)$ is equivalent to the type of natural numbers with its canonical identity type.

This implies that the modulus relation is valued in h-propositions and is a family of decidable equivalence relations indexed by $k$.

References

Last revised on October 11, 2022 at 22:52:33. See the history of this page for a list of all contributions to it.