Является ли эта формулировка по модулю набора?

Question

В кубической библиотеке Agda определен тип Modulo, подобный этому :

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 s и pre-step s не имеет значения; но как это будет оформлено?

Answer 1

Исходя из комментария @ Андраса Ковача, выясняется, что Modulo n действительно является h-множеством, а есть доказательство в стандартной библиотеке , я просто пропустил его:)

Доказательство в основном выглядит так:

• Modulo 0 изоморфно c до ℕ, поскольку NonZero 0 пусто (поэтому у нас есть только embed значения).
• Modulo (suc k) изоморфно c до Fin (suc k), в основном, применяя достаточно pre-step с, пока мы не получим embed n с n < k. Это длинное техническое доказательство, использующее собственный модуль .

И тогда, конечно, и ℕ, и Fin (suc k) являются дискретными, следовательно, h-наборы сами.