Is this formulation of Modulo a Set?

Question

The Cubical Agda library defined a Modulo type like this:

data Modulo (k : ℕ) : Type₀ where
  embed : (n : ℕ) → Modulo k
  pre-step : NonZero k → (n : ℕ) → embed n ≡ embed (k + n)

Is this a Set?

Hand-wavingly, I can see that any path is a composition of refls and pre-steps, taking the form embed n ≡ embed (m * k + n); and since _+_ is associative and 0 +_ ≡ id, the structure of how refls and pre-steps are combined doesn't matter; but how would that be formalized?

Answer 1

Based on @András Kovács's comment, turns out Modulo n is indeed a h-set and there is a proof in the standard library, I just missed it :)

The proof basically goes like this:

• Modulo 0 is isomorphic to ℕ since NonZero 0 is empty (so we only have embed values).
• Modulo (suc k) is isomorphic to Fin (suc k) basically by applying enough pre-steps until we get embed n with n < k. This is a long-winded technical proof taking up its own module.

And then of course both ℕ and Fin (suc k) are discrete, hence h-sets themselves.