{-# OPTIONS --safe #-}
module Cubical.Algebra.CommMonoid.Properties where

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

open import Cubical.Data.Sigma

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.CommMonoid.Base

private
  variable
     ℓ' : Level

module _
    (M : CommMonoid )
    (P :  M   hProp ℓ')
    where
  open CommMonoidStr (snd M)
  module _
    (·Closed : (x y :  M )   P x    P y    P (x · y) )
    (εContained :  P ε )
    where
    private
      subtype = Σ[ x   M  ]  P x 

    makeSubCommMonoid : CommMonoid _
    fst makeSubCommMonoid = subtype
    CommMonoidStr.ε (snd makeSubCommMonoid) = ε , εContained
    CommMonoidStr._·_ (snd makeSubCommMonoid) (x , xContained) (y , yContained) =
      (x · y) , ·Closed x y xContained yContained
    IsCommMonoid.isMonoid (CommMonoidStr.isCommMonoid (snd makeSubCommMonoid)) =
      makeIsMonoid
        (isOfHLevelΣ 2 is-set λ _  isProp→isSet (snd (P _)))
         x y z  Σ≡Prop  _  snd (P _)) (·Assoc (fst x) (fst y) (fst z)))
         x  Σ≡Prop  _  snd (P _)) (·IdR (fst x)))
        λ x  Σ≡Prop  _  snd (P _)) (·IdL (fst x))
    IsCommMonoid.·Comm (CommMonoidStr.isCommMonoid (snd makeSubCommMonoid)) =
      λ x y  Σ≡Prop  _  snd (P _)) (·Comm (fst x) (fst y))

module CommMonoidTheory (M' : CommMonoid ) where
 open CommMonoidStr (snd M')
 private M =  M' 

 commAssocl : (x y z : M)  x · (y · z)  y · (x · z)
 commAssocl x y z = ·Assoc x y z ∙∙ cong ( z) (·Comm x y) ∙∙ sym (·Assoc y x z)

 commAssocr : (x y z : M)  x · y · z  x · z · y
 commAssocr x y z = sym (·Assoc x y z) ∙∙ cong (x ·_) (·Comm y z) ∙∙ ·Assoc x z y


 commAssocr2 : (x y z : M)  x · y · z  z · y · x
 commAssocr2 x y z = commAssocr _ _ _ ∙∙ cong ( y) (·Comm _ _) ∙∙ commAssocr _ _ _

 commAssocSwap : (x y z w : M)  (x · y) · (z · w)  (x · z) · (y · w)
 commAssocSwap x y z w = ·Assoc (x · y) z w ∙∙ cong ( w) (commAssocr x y z)
                                               ∙∙ sym (·Assoc (x · z) y w)