agda - Modulo 的这个公式是一个集合吗？

Question

Cubical Agda 库 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)

这是一套吗？

挥挥手，我可以看到任何路径都是 refl s 和 pre-step s 的组合，采用 embed n ≡ embed (m * k + n) 形式；和
由于 _+_ 和 0 +_ ≡ id 是关联的，因此 refl 和 pre-step 的组合结构无关紧要；但这将如何正式化？

Answer 1

根据@András Kovács 的评论，结果 Modulo n 确实是一个 h-set 和 there is a proof in the standard library ，我只是错过了:)

证明基本上是这样的:

Modulo 0 与 ℕ 同构，因为 NonZero 0 是空的(所以我们只有 embed 值)。

Modulo (suc k) 与 Fin (suc k) 同构，基本上通过应用足够的 pre-step 直到我们得到 embed n 和 n < k 。 This is a long-winded technical proof taking up its own module 。

然后当然 ℕ 和 Fin (suc k) 都是离散的，因此 h-sets 本身。