module ring-0001 where open import MLTT.Spartan open import UF.Subsingletons open import UF.Subsingletons-Properties open import ring-0000 open Ring {{...}}
Trivial ring 就像前面群論提過的 trivial group，在 trivial ring 裡加法、乘法都一樣，因為作為只有一個元素的集合，能選擇的 n-元運算都只有一個。 也因此下面的 terms 幾乎都可以由 agda 自動填滿
trivial-ring : Ring (𝟙 {𝓤}) trivial-ring .size = props-are-sets 𝟙-is-prop trivial-ring ._⊕_ _ _ = ⋆ trivial-ring .𝟘R = ⋆ trivial-ring .⊕-assoc = λ x y z → refl trivial-ring .0l-neu = λ x → refl trivial-ring .0r-neu = λ x → refl trivial-ring .-_ _ = ⋆ trivial-ring .cancel = refl , refl trivial-ring .⊕-comm = refl trivial-ring ._⊗_ _ _ = ⋆ trivial-ring .⊗-assoc = λ x y z → refl trivial-ring .𝟙R = ⋆ trivial-ring .1l-neu = λ x → refl trivial-ring .1r-neu = λ x → refl trivial-ring .distrib1 = refl trivial-ring .distrib2 = refl