cubical/Cubical/Algebra/CommRing/Instances/QuoQRationals.agda at cf04fb854990c7c00ec3fb3c22d692f7986bf888 · broughjt/cubical · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
{-

ℚ (the QuoQ version) is a Commutative Ring

-}
module Cubical.Algebra.CommRing.Instances.QuoQRationals where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.CommRing
open import Cubical.Data.Rationals.MoreRationals.QuoQ
  renaming (ℚ to ℚType ; _+_ to _+ℚ_; _·_ to _·ℚ_; -_ to -ℚ_)

open CommRingStr


ℚCommRing : CommRing ℓ-zero
ℚCommRing .fst = ℚType
ℚCommRing .snd .0r = 0
ℚCommRing .snd .1r = 1
ℚCommRing .snd ._+_ = _+ℚ_
ℚCommRing .snd ._·_ = _·ℚ_
ℚCommRing .snd .-_ = -ℚ_
ℚCommRing .snd .isCommRing = isCommRingℚ
  where
  abstract
    isCommRingℚ : IsCommRing 0 1 _+ℚ_ _·ℚ_ -ℚ_
    isCommRingℚ = makeIsCommRing
      isSetℚ +-assoc +-identityʳ
      +-inverseʳ +-comm ·-assoc
      ·-identityʳ (λ x y z → sym (·-distribˡ x y z)) ·-comm