{-

  Lets do some algebraic structures. That's always fun!

-}

module Structures where

open import Relation.Binary.PropositionalEquality

{-

  We'll start out with monoids.

  We can't do ML-style sharing, so we have to go Pebble-style.

-}

-- Since we don't know what things we may want to share,
-- we parameterize over everything but the laws.
record IsMonoid {A : Set}(_∙_ : A  A  A)( : A) : Set where
  field
    left-id  :  x    x  x
    right-id :  x  x    x
    assoc    :  x y z  (x  y)  z  x  (y  z)

-- We can then pack up an IsMonoid record with its parameters
-- to get a Monoid
record Monoid : Set₁ where
  field
    C   : Set
    _∙_ : C  C  C
       : C
    isMonoid : IsMonoid _∙_ 

  -- We can unpack the IsMonoid record to make the monoid laws
  -- available directly from Monoid.
  open IsMonoid isMonoid public


module Test (A : Monoid) where
  open module M = Monoid A

  -- test : Set
  -- test = {!M!}

  -- C-c C-o in the hole shows us the contents of the Monoid module:
  --   Modules
  --   Names
  --     _∙_      : C → C → C
  --     C        : Set
  --     assoc    : (x y z : C) → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)
  --     isMonoid : IsMonoid _∙_ ∅
  --     left-id  : (x : C) → ∅ ∙ x ≡ x
  --     right-id : (x : C) → x ∙ ∅ ≡ x
  --     ∅        : C

{-

  Let's keep going. Now groups.

-}

record IsGroup {A}(_∙_ : A  A  A)( : A)(_⁻¹ : A  A) : Set where
  field
    isMonoid  : IsMonoid _∙_ 
    left-inv  :  x  (x ⁻¹)  x  
    right-inv :  x  x  (x ⁻¹)  

  -- Unpacking isMonoid gives us a cheap form of record extension.
  open IsMonoid isMonoid public

record Group : Set₁ where
  field
    C   : Set
    _∙_ : C  C  C
       : C
    _⁻¹ : C  C
    isGroup : IsGroup _∙_  _⁻¹

  open IsGroup isGroup public

  -- A group is also a monoid, but there's no Monoid field in our Group
  -- (due to Pebble-style sharing). We can easily define one, though.
  monoid : Monoid
  monoid = record { isMonoid = isMonoid }  -- inferrable fields can be omitted


{-

  Abelian groups are next.

-}

record IsAbelianGroup {A : Set}(_∙_ : A  A  A)( : A)(_⁻¹ : A  A) : Set
       where
  field
    isGroup : IsGroup _∙_  _⁻¹
    commute :  x y  x  y  y  x

  open IsGroup isGroup public


record AbelianGroup : Set₁ where
  field
    C   : Set
    _∙_ : C  C  C
       : C
    _⁻¹ : C  C
    isAbelianGroup : IsAbelianGroup _∙_  _⁻¹

  open IsAbelianGroup isAbelianGroup public

  group : Group
  group = record { isGroup = isGroup }

  -- To get access to the underlying Monoid we can open the
  -- Group we just defined.
  open Group group public using (monoid)


{-

  Finally, let's do rings.

-}

record IsRing {A : Set}(`0 `1 : A)(_+_ _*_ : A  A  A)(-_ : A  A) : Set where
  field
    +-isAbelianGroup : IsAbelianGroup _+_ `0 -_
    *-isMonoid       : IsMonoid _*_ `1
    left-distr  :  x y z  x * (y + z)  (x * y) + (x * z)
    right-distr :  x y z  (x + y) * z  (x * z) + (y * z)

  -- Now we have two monoids, so we had better rename the laws to
  -- avoid name clashes.
  open IsMonoid *-isMonoid public
    renaming ( assoc    to *-assoc
             ; left-id  to *-left-id
             ; right-id to *-right-id )

  open IsAbelianGroup +-isAbelianGroup public
    renaming ( assoc     to +-assoc
             ; left-id   to +-left-id
             ; right-id  to +-right-id
             ; commute   to +-commute
             ; left-inv  to +-left-inv
             ; right-inv to +-right-inv
             ; isMonoid  to +-isMonoid
             ; isGroup   to +-isGroup )

record Ring : Set₁ where
  field
    C       : Set
    `0 `1   : C
    _+_ _*_ : C  C  C
    -_      : C  C
    isRing : IsRing `0 `1 _+_ _*_ -_

  open IsRing isRing public

  +-abelianGroup : AbelianGroup
  +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }

  *-monoid : Monoid
  *-monoid = record { isMonoid = *-isMonoid }

  -- Getting access to the group and monoid for _+_
  open AbelianGroup +-abelianGroup public
    using ()
    renaming ( monoid to +-monoid
             ; group  to +-group )