-- §──────────────────────────────────────────────────────────────────
-- Modules required for specifying the parameters of this module
-- §──────────────────────────────────────────────────────────────────

import Algebra as A
import Level as L

-- §──────────────────────────────────────────────────────────────────
-- This module
-- §──────────────────────────────────────────────────────────────────

module My.Surd.CommutativeMonoid {𝓁 𝓂 : L.Level}
  (cm : A.CommutativeMonoid 𝓁 𝓂)
  where

-- §──────────────────────────────────────────────────────────────────
-- Other required modules
-- §──────────────────────────────────────────────────────────────────

import Data.Sum as DS
import Relation.Binary.EqReasoning as RBER
import Relation.Nullary as RN
import Relation.Unary as RU

open DS using (_⊎_)
open L using (_⊔_)

private
  module CM = A.CommutativeMonoid cm

open CM using (_≈_ ; _∙_)

-- §──────────────────────────────────────────────────────────────────
-- The basic definitions
-- §──────────────────────────────────────────────────────────────────

record Unit (p : CM.Carrier) : Set (𝓁 ⊔ 𝓂)
  where
    field
      inv : CM.Carrier
      pf : p ∙ inv ≈ CM.ε

infix  _∣_
record _∣_ (p a : CM.Carrier) : Set (𝓁 ⊔ 𝓂)
  where
    field
      quotient : CM.Carrier
      pf : p ∙ quotient ≈ a

record Prime (p : CM.Carrier) : Set (𝓁 ⊔ 𝓂)
  where
    field
      nonUnit : RN.¬ Unit p
      prePrime : {a b : CM.Carrier} → p ∣ a ∙ b → p ∣ a ⊎ p ∣ b

square : CM.Carrier → CM.Carrier
square x = x ∙ x

record hasRatSqrt (p : CM.Carrier) : Set (𝓁 ⊔ 𝓂)
  where
    field
      num : CM.Carrier
      den : CM.Carrier
      pf : p ∙ square den ≈ square num

Surd : RU.Pred CM.Carrier (𝓁 ⊔ 𝓂)
Surd p = RN.¬ hasRatSqrt p

thm₁ : Unit CM.ε
thm₁ = record { inv = CM.ε ; pf = CM.identityˡ CM.ε }

thm₂ : {p q : CM.Carrier} → Unit p → p ≈ q → Unit q
thm₂ {p} {q} unitp p≈q = record { inv = inv ; pf = pf }
  where
    module U = Unit unitp
    inv : CM.Carrier
    inv = U.inv
    pf : q ∙ inv ≈ CM.ε
    pf =
      begin
        q ∙ inv ≈⟨ CM.∙-cong (CM.sym p≈q) CM.refl ⟩
        p ∙ inv ≈⟨ U.pf ⟩
        CM.ε ∎
      where open RBER CM.setoid