module ring-0001 where open import MLTT.Spartan open import UF.Subsingletons open import UF.Subsingletons-Properties open import UF.Equiv open import ring-0000 open Ring {{...}} open import ring-0002
Trivial ring 就像前面群論提過的 trivial group，在 trivial ring 裡加法、乘法都一樣，因為作為只有一個元素的集合，能選擇的 n-元運算都只有一個。 也因此下面的 terms 幾乎都可以由 agda 自動填滿
trivial-ring : Ring (𝟙 {𝓤}) trivial-ring .size = props-are-sets 𝟙-is-prop trivial-ring ._+ᴿ_ _ _ = ⋆ trivial-ring .0r = ⋆ trivial-ring .+-assoc = λ x y z → refl trivial-ring .+-neuL = λ x → refl trivial-ring .+-neuR = λ x → refl trivial-ring .-_ _ = ⋆ trivial-ring .cancel = refl trivial-ring .+-comm = λ x y → refl trivial-ring ._·_ _ _ = ⋆ trivial-ring .·-assoc = λ x y z → refl trivial-ring .1r = ⋆ trivial-ring .·-neuL = λ x → refl trivial-ring .·-neuR = λ x → refl trivial-ring .distribL = refl trivial-ring .distribR = refl
事實上如果 Ring R 的 1 = 0，那麼 R 只有一個元素
0=1-leads-trivial-ring : {R : 𝓤 ̇ } → {{∈R : Ring R}} → 1r ＝ 0r → 𝟙 {𝓤} ≃ R 0=1-leads-trivial-ring {𝓤}{R} 1=0 = (λ _ → 0r) , (ι , λ x → every-elem-is-0 x ⁻¹) , (ι , λ _ → refl) where ι : R → 𝟙 {𝓤} ι _ = ⋆ every-elem-is-0 : ∀ (x : R) → x ＝ 0r every-elem-is-0 x = x ＝⟨ ·-neuR x ⁻¹ ⟩ x · 1r ＝⟨ ap (x ·_) 1=0 ⟩ x · 0r ＝⟨ lemma-1 x .pr₁ ⟩
這裡雖然用了等一下才要證明的定理，但任何元素乘上 0 等於 0 應該是很直覺的想法
0r ∎