{-# OPTIONS --safe #-}
module Cubical.Algebra.CommMonoid.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.Monoid

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 IsCommMonoid {M : Type }
                    (ε : M) (_·_ : M  M  M) : Type  where
  constructor iscommmonoid

  field
    isMonoid : IsMonoid ε _·_
    ·Comm     : (x y : M)  x · y  y · x

  open IsMonoid isMonoid public

unquoteDecl IsCommMonoidIsoΣ = declareRecordIsoΣ IsCommMonoidIsoΣ (quote IsCommMonoid)

record CommMonoidStr (M : Type ) : Type  where
  constructor commmonoidstr

  field
    ε            : M
    _·_          : M  M  M
    isCommMonoid : IsCommMonoid ε _·_

  infixl 7 _·_

  open IsCommMonoid isCommMonoid public

CommMonoid :    Type (ℓ-suc )
CommMonoid  = TypeWithStr  CommMonoidStr

makeIsCommMonoid : {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)
                 (·Comm    : (x y : M)  x · y  y · x)
                IsCommMonoid ε _·_
IsCommMonoid.isMonoid (makeIsCommMonoid is-setM ·Assoc ·IdR ·Comm) =
  makeIsMonoid is-setM ·Assoc ·IdR  x  ·Comm _ _  ·IdR x)
IsCommMonoid.·Comm (makeIsCommMonoid is-setM ·Assoc ·IdR ·Comm) = ·Comm

makeCommMonoid : {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)
               (·Comm    : (x y : M)  x · y  y · x)
              CommMonoid 
fst (makeCommMonoid ε _·_ is-setM ·Assoc ·IdR ·Comm) = _
CommMonoidStr.ε (snd (makeCommMonoid ε _·_ is-setM ·Assoc ·IdR ·Comm)) = ε
CommMonoidStr._·_ (snd (makeCommMonoid ε _·_ is-setM ·Assoc ·IdR ·Comm)) = _·_
CommMonoidStr.isCommMonoid (snd (makeCommMonoid ε _·_ is-setM ·Assoc ·IdR ·Comm)) =
  makeIsCommMonoid is-setM ·Assoc ·IdR ·Comm

CommMonoidStr→MonoidStr : {A : Type }  CommMonoidStr A  MonoidStr A
CommMonoidStr→MonoidStr (commmonoidstr _ _ H) = monoidstr _ _ (IsCommMonoid.isMonoid H)

CommMonoid→Monoid : CommMonoid   Monoid 
CommMonoid→Monoid (_ , commmonoidstr  _ _ M) = _ , monoidstr _ _ (IsCommMonoid.isMonoid M)

CommMonoidHom : (L : CommMonoid ) (M : CommMonoid ℓ')  Type (ℓ-max  ℓ')
CommMonoidHom L M = MonoidHom (CommMonoid→Monoid L) (CommMonoid→Monoid M)

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

CommMonoidEquiv : (M : CommMonoid ) (N : CommMonoid ℓ')  Type (ℓ-max  ℓ')
CommMonoidEquiv M N = Σ[ e  (M .fst  N .fst) ] IsCommMonoidEquiv (M .snd) e (N .snd)

isPropIsCommMonoid : {M : Type } (ε : M) (_·_ : M  M  M)
              isProp (IsCommMonoid ε _·_)
isPropIsCommMonoid ε _·_  =
  isOfHLevelRetractFromIso 1 IsCommMonoidIsoΣ
    (isPropΣ (isPropIsMonoid ε _·_)
             λ mon  isPropΠ2  _ _  mon .is-set _ _))
  where
  open IsMonoid

𝒮ᴰ-CommMonoid : DUARel (𝒮-Univ ) CommMonoidStr 
𝒮ᴰ-CommMonoid =
  𝒮ᴰ-Record (𝒮-Univ _) IsCommMonoidEquiv
    (fields:
      data[ ε  autoDUARel _ _  presε ]
      data[ _·_  autoDUARel _ _  pres· ]
      prop[ isCommMonoid   _ _  isPropIsCommMonoid _ _) ])
  where
  open CommMonoidStr
  open IsMonoidHom

CommMonoidPath : (M N : CommMonoid )  CommMonoidEquiv M N  (M  N)
CommMonoidPath =  𝒮ᴰ-CommMonoid .UARel.ua