module Cubical.Algebra.Monoid.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Algebra.Semigroup

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Reflection.RecordEquiv

open Iso

private
  variable
    ℓ ℓ' : Level

record IsMonoid {A : Type ℓ} (ε : A) (_·_ : A → A → A) : Type ℓ where
  constructor ismonoid

  field
    isSemigroup : IsSemigroup _·_
    ·IdR : (x : A) → x · ε ≡ x
    ·IdL : (x : A) → ε · x ≡ x

  open IsSemigroup isSemigroup public

unquoteDecl IsMonoidIsoΣ = declareRecordIsoΣ IsMonoidIsoΣ (quote IsMonoid)

record MonoidStr (A : Type ℓ) : Type ℓ where
  constructor monoidstr

  field
    ε        : A
    _·_      : A → A → A
    isMonoid : IsMonoid ε _·_

  infixl  _·_

  open IsMonoid isMonoid public

Monoid : ∀ ℓ → Type (ℓ-suc ℓ)
Monoid ℓ = TypeWithStr ℓ MonoidStr

monoid : (A : Type ℓ) (ε : A) (_·_ : A → A → A) (h : IsMonoid ε _·_) → Monoid ℓ
monoid A ε _·_ h = A , monoidstr ε _·_ h

-- Easier to use constructors

makeIsMonoid : {M : Type ℓ} {ε : M} {_·_ : M → M → M}
               (is-setM : isSet M)
               (·Assoc : (x y z : M) → x · (y · z) ≡ (x · y) · z)
               (·IdR : (x : M) → x · ε ≡ x)
               (·IdL : (x : M) → ε · x ≡ x)
             → IsMonoid ε _·_
IsMonoid.isSemigroup (makeIsMonoid is-setM ·Assoc ·IdR ·IdL) = issemigroup is-setM ·Assoc
IsMonoid.·IdR (makeIsMonoid is-setM ·Assoc ·IdR ·IdL) = ·IdR
IsMonoid.·IdL (makeIsMonoid is-setM ·Assoc ·IdR ·IdL) = ·IdL

makeMonoid : {M : Type ℓ} (ε : M) (_·_ : M → M → M)
             (is-setM : isSet M)
             (·Assoc : (x y z : M) → x · (y · z) ≡ (x · y) · z)
             (·IdR : (x : M) → x · ε ≡ x)
             (·IdL : (x : M) → ε · x ≡ x)
           → Monoid ℓ
makeMonoid ε _·_ is-setM ·Assoc ·IdR ·IdL =
  monoid _ ε _·_ (makeIsMonoid is-setM ·Assoc ·IdR ·IdL)

record IsMonoidHom {A : Type ℓ} {B : Type ℓ'}
  (M : MonoidStr A) (f : A → B) (N : MonoidStr B)
  : Type (ℓ-max ℓ ℓ')
  where

  constructor monoidequiv

  -- Shorter qualified names
  private
    module M = MonoidStr M
    module N = MonoidStr N

  field
    presε : f M.ε ≡ N.ε
    pres· : (x y : A) → f (x M.· y) ≡ f x N.· f y

MonoidHom : (L : Monoid ℓ) (M : Monoid ℓ') → Type (ℓ-max ℓ ℓ')
MonoidHom L M = Σ[ f ∈ (⟨ L ⟩ → ⟨ M ⟩) ] IsMonoidHom (L .snd) f (M .snd)

IsMonoidEquiv : {A : Type ℓ} {B : Type ℓ'} (M : MonoidStr A) (e : A ≃ B) (N : MonoidStr B)
  → Type (ℓ-max ℓ ℓ')
IsMonoidEquiv M e N = IsMonoidHom M (e .fst) N

MonoidEquiv : (M : Monoid ℓ) (N : Monoid ℓ') → Type (ℓ-max ℓ ℓ')
MonoidEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsMonoidEquiv (M .snd) e (N .snd)

-- We now extract the important results from the above module

isPropIsMonoid : {M : Type ℓ} (ε : M) (_·_ : M → M → M) → isProp (IsMonoid ε _·_)
isPropIsMonoid ε _·_ =
  isOfHLevelRetractFromIso  IsMonoidIsoΣ
    (isPropΣ (isPropIsSemigroup _·_)
             (λ semi → isProp× (isPropΠ (λ _ → is-set semi _ _))
                                (isPropΠ (λ _ → is-set semi _ _))))
  where
  open IsSemigroup

𝒮ᴰ-Monoid : DUARel (𝒮-Univ ℓ) MonoidStr ℓ
𝒮ᴰ-Monoid =
  𝒮ᴰ-Record (𝒮-Univ _) IsMonoidEquiv
    (fields:
      data[ ε ∣ autoDUARel _ _ ∣ presε ]
      data[ _·_ ∣ autoDUARel _ _ ∣ pres· ]
      prop[ isMonoid ∣ (λ _ _ → isPropIsMonoid _ _) ])
  where
  open MonoidStr
  open IsMonoidHom

MonoidPath : (M N : Monoid ℓ) → MonoidEquiv M N ≃ (M ≡ N)
MonoidPath = ∫ 𝒮ᴰ-Monoid .UARel.ua

module MonoidTheory {ℓ} (M : Monoid ℓ) where

  open MonoidStr (snd M)

  -- Added for its use in groups
  -- If there exists a inverse of an element it is unique
  inv-lemma : (x y z : ⟨ M ⟩) → y · x ≡ ε → x · z ≡ ε → y ≡ z
  inv-lemma x y z left-inverse right-inverse =
    y           ≡⟨ sym (·IdR y) ⟩
    y · ε       ≡⟨ congR _·_ (sym right-inverse) ⟩
    y · (x · z) ≡⟨ ·Assoc y x z ⟩
    (y · x) · z ≡⟨ congL _·_ left-inverse ⟩
    ε · z       ≡⟨ ·IdL z ⟩
    z ∎

  -- Added for its use in division rings
  hasInverse : (x : ⟨ M ⟩) → Type ℓ
  hasInverse x = Σ[ -x ∈ ⟨ M ⟩ ] (-x · x ≡ ε) × (x · -x ≡ ε)

  isPropHasInverse : ∀ x → isProp (hasInverse x)
  isPropHasInverse x (y , invly , _) (z , _ , invrz)
    = Σ≡Prop (λ a → isProp× (is-set (a · x) ε)
                             (is-set (x · a) ε))
              (inv-lemma x y z invly invrz)