{-# OPTIONS --safe #-}
{-
  This used to be the default definition of CommAlgebra.
  The plan is to remove duplicated constructions based on this definition.
-}
module Cubical.Algebra.CommAlgebra.AsModule.Base where

open import Cubical.Foundations.Prelude
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.Algebra.Monoid
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Algebra

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

private
  variable
    ℓ ℓ' ℓ'' : Level

record IsCommAlgebra (R : CommRing ℓ) {A : Type ℓ'}
                     (0a : A) (1a : A)
                     (_+_ : A → A → A) (_·_ : A → A → A) (-_ : A → A)
                     (_⋆_ : ⟨ R ⟩ → A → A) : Type (ℓ-max ℓ ℓ') where
  no-eta-equality

  field
    isAlgebra : IsAlgebra (CommRing→Ring R) 0a 1a _+_ _·_ -_ _⋆_
    ·Comm    : (x y : A) → x · y ≡ y · x

  open IsAlgebra isAlgebra public

unquoteDecl IsCommAlgebraIsoΣ = declareRecordIsoΣ IsCommAlgebraIsoΣ (quote IsCommAlgebra)

record CommAlgebraStr (R : CommRing ℓ) (A : Type ℓ') : Type (ℓ-max ℓ ℓ') where
  no-eta-equality

  field
    0a             : A
    1a             : A
    _+_            : A → A → A
    _·_            : A → A → A
    -_             : A → A
    _⋆_            : ⟨ R ⟩ → A → A
    isCommAlgebra      : IsCommAlgebra R 0a 1a _+_ _·_ -_ _⋆_

  open IsCommAlgebra isCommAlgebra public

  infix   -_
  infixl  _·_
  infixl  _⋆_
  infixl  _+_

unquoteDecl CommAlgebraStrIsoΣ = declareRecordIsoΣ CommAlgebraStrIsoΣ (quote CommAlgebraStr)

CommAlgebra : (R : CommRing ℓ) → ∀ ℓ' → Type (ℓ-max ℓ (ℓ-suc ℓ'))
CommAlgebra R ℓ' = Σ[ A ∈ Type ℓ' ] CommAlgebraStr R A

module _ {R : CommRing ℓ} where
  open CommRingStr (snd R) using (1r) renaming (_+_ to _+r_; _·_ to _·s_)

  CommAlgebraStr→AlgebraStr : {A : Type ℓ'} → CommAlgebraStr R A → AlgebraStr (CommRing→Ring R) A
  CommAlgebraStr→AlgebraStr {A = A} cstr = x
    where open AlgebraStr
          x : AlgebraStr (CommRing→Ring R) A
          0a x = _
          1a x = _
          _+_ x = _
          _·_ x = _
          - x = _
          _⋆_ x = _
          isAlgebra x = IsCommAlgebra.isAlgebra (CommAlgebraStr.isCommAlgebra cstr)

  CommAlgebra→Algebra : (A : CommAlgebra R ℓ') → Algebra (CommRing→Ring R) ℓ'
  fst (CommAlgebra→Algebra A) = fst A
  snd (CommAlgebra→Algebra A) = CommAlgebraStr→AlgebraStr (snd A)

  CommAlgebra→CommRing : (A : CommAlgebra R ℓ') → CommRing ℓ'
  CommAlgebra→CommRing (A , str) = x
    where open CommRingStr
          open CommAlgebraStr
          x : CommRing _
          fst x = A
          0r (snd x) = _
          1r (snd x) = _
          _+_ (snd x) = _
          _·_ (snd x) = _
          - snd x = _
          IsCommRing.isRing (isCommRing (snd x)) = RingStr.isRing (Algebra→Ring (_ , CommAlgebraStr→AlgebraStr str) .snd)
          IsCommRing.·Comm (isCommRing (snd x)) = CommAlgebraStr.·Comm  str

  module _
      {A : Type ℓ'} {0a 1a : A}
      {_+_ _·_ : A → A → A} { -_ : A → A} {_⋆_ : ⟨ R ⟩ → A → A}
      (isSet-A : isSet A)
      (+Assoc  :  (x y z : A) → x + (y + z) ≡ (x + y) + z)
      (+IdR    : (x : A) → x + 0a ≡ x)
      (+InvR   : (x : A) → x + (- x) ≡ 0a)
      (+Comm   : (x y : A) → x + y ≡ y + x)
      (·Assoc  :  (x y z : A) → x · (y · z) ≡ (x · y) · z)
      (·IdL    : (x : A) → 1a · x ≡ x)
      (·DistL+ : (x y z : A) → (x + y) · z ≡ (x · z) + (y · z))
      (·Comm   : (x y : A) → x · y ≡ y · x)
      (⋆Assoc  : (r s : ⟨ R ⟩) (x : A) → (r ·s s) ⋆ x ≡ r ⋆ (s ⋆ x))
      (⋆DistR+ : (r : ⟨ R ⟩) (x y : A) → r ⋆ (x + y) ≡ (r ⋆ x) + (r ⋆ y))
      (⋆DistL+ : (r s : ⟨ R ⟩) (x : A) → (r +r s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x))
      (⋆IdL    : (x : A) → 1r ⋆ x ≡ x)
      (⋆AssocL : (r : ⟨ R ⟩) (x y : A) → (r ⋆ x) · y ≡ r ⋆ (x · y))
    where


    makeIsCommAlgebra : IsCommAlgebra R 0a 1a _+_ _·_ -_ _⋆_
    makeIsCommAlgebra .IsCommAlgebra.isAlgebra = makeIsAlgebra
     isSet-A
     +Assoc +IdR +InvR +Comm
     ·Assoc ·IdR ·IdL ·DistR+ ·DistL+
     ⋆Assoc
     ⋆DistR+
     ⋆DistL+
     ⋆IdL
     ⋆AssocR
     ⋆AssocL
       where
       ·IdR : _
       ·IdR x = x · 1a ≡⟨ ·Comm _ _ ⟩ 1a · x ≡⟨ ·IdL _ ⟩ x ∎
       ·DistR+ : _
       ·DistR+ x y z = x · (y + z)       ≡⟨ ·Comm _ _ ⟩
                       (y + z) · x       ≡⟨ ·DistL+ _ _ _ ⟩
                       (y · x) + (z · x) ≡⟨ cong (λ u → (y · x) + u) (·Comm _ _) ⟩
                       (y · x) + (x · z) ≡⟨ cong (λ u → u + (x · z)) (·Comm _ _) ⟩
                       (x · y) + (x · z) ∎
       ⋆AssocR : _
       ⋆AssocR r x y = r ⋆ (x · y) ≡⟨ cong (λ u → r ⋆ u) (·Comm _ _) ⟩
                       r ⋆ (y · x) ≡⟨ sym (⋆AssocL _ _ _) ⟩
                       (r ⋆ y) · x ≡⟨ ·Comm _ _ ⟩
                       x · (r ⋆ y) ∎
    makeIsCommAlgebra .IsCommAlgebra.·Comm = ·Comm

  makeCommAlgebraStr :
    (A : Type ℓ') (0a 1a : A)
    (_+_ _·_ : A → A → A) ( -_ : A → A) (_⋆_ : ⟨ R ⟩ → A → A)
    (isCommAlg : IsCommAlgebra R 0a 1a _+_ _·_ -_ _⋆_)
    → CommAlgebraStr R A
  makeCommAlgebraStr A 0a 1a _+_ _·_ -_ _⋆_ isCommAlg =
    record
      { 0a = 0a
      ; 1a = 1a
      ; _+_ = _+_
      ; _·_ = _·_
      ; -_ =  -_
      ; _⋆_ = _⋆_
      ; isCommAlgebra = isCommAlg
      }

  module _ (S : CommRing ℓ') where
    open CommRingStr (snd S) renaming (1r to 1S)
    open CommRingStr (snd R) using () renaming (_·_ to _·R_; _+_ to _+R_; 1r to 1R)

    module _
        (_⋆_ : fst R → fst S → fst S)
        (·Assoc⋆ : (r s : fst R) (x : fst S) → (r ·R s) ⋆ x ≡ r ⋆ (s ⋆ x))
        (⋆DistR+ : (r : fst R) (x y : fst S) → r ⋆ (x + y) ≡ (r ⋆ x) + (r ⋆ y))
        (⋆DistL+ : (r s : fst R) (x : fst S) → (r +R s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x))
        (⋆IdL    : (x : fst S) → 1R ⋆ x ≡ x)
        (⋆AssocL : (r : fst R) (x y : fst S) → (r ⋆ x) · y ≡ r ⋆ (x · y))
      where

      commAlgebraFromCommRing : CommAlgebra R ℓ'
      commAlgebraFromCommRing .fst = fst S
      commAlgebraFromCommRing .snd .CommAlgebraStr.0a = 0r
      commAlgebraFromCommRing .snd .CommAlgebraStr.1a = 1S
      commAlgebraFromCommRing .snd .CommAlgebraStr._+_ = _+_
      commAlgebraFromCommRing .snd .CommAlgebraStr._·_ = _·_
      commAlgebraFromCommRing .snd .CommAlgebraStr.-_ = -_
      commAlgebraFromCommRing .snd .CommAlgebraStr._⋆_ = _⋆_
      commAlgebraFromCommRing .snd .CommAlgebraStr.isCommAlgebra =
        makeIsCommAlgebra is-set +Assoc +IdR +InvR +Comm ·Assoc ·IdL ·DistL+ ·Comm
                                    ·Assoc⋆ ⋆DistR+ ⋆DistL+ ⋆IdL ⋆AssocL

      commAlgebraFromCommRing→CommRing : CommAlgebra→CommRing commAlgebraFromCommRing ≡ S
      -- Note that this is not definitional: the proofs of the axioms might differ.
      commAlgebraFromCommRing→CommRing i .fst  = ⟨ S ⟩
      commAlgebraFromCommRing→CommRing i .snd .CommRingStr.0r = 0r
      commAlgebraFromCommRing→CommRing i .snd .CommRingStr.1r = 1S
      commAlgebraFromCommRing→CommRing i .snd .CommRingStr._+_ = _+_
      commAlgebraFromCommRing→CommRing i .snd .CommRingStr._·_ = _·_
      commAlgebraFromCommRing→CommRing i .snd .CommRingStr.-_ = -_
      commAlgebraFromCommRing→CommRing i .snd .CommRingStr.isCommRing =
        isProp→PathP (λ i → isPropIsCommRing _ _ _ _ _)
          (CommRingStr.isCommRing (snd (CommAlgebra→CommRing commAlgebraFromCommRing)))
          isCommRing
          i

  IsCommAlgebraEquiv : {A : Type ℓ'} {B : Type ℓ''}
    (M : CommAlgebraStr R A) (e : A ≃ B) (N : CommAlgebraStr R B)
    → Type _
  IsCommAlgebraEquiv M e N =
    IsAlgebraHom (CommAlgebraStr→AlgebraStr M) (e .fst) (CommAlgebraStr→AlgebraStr N)

  CommAlgebraEquiv : (M : CommAlgebra R ℓ') (N : CommAlgebra R ℓ'') → Type _
  CommAlgebraEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsCommAlgebraEquiv (M .snd) e (N .snd)

  IsCommAlgebraHom : {A : Type ℓ'} {B : Type ℓ''}
    (M : CommAlgebraStr R A) (f : A → B) (N : CommAlgebraStr R B)
    → Type _
  IsCommAlgebraHom M f N =
    IsAlgebraHom (CommAlgebraStr→AlgebraStr M) f (CommAlgebraStr→AlgebraStr N)

  CommAlgebraHom : (M : CommAlgebra R ℓ') (N : CommAlgebra R ℓ'') → Type _
  CommAlgebraHom M N = Σ[ f ∈ (⟨ M ⟩ → ⟨ N ⟩) ] IsCommAlgebraHom (M .snd) f (N .snd)

  CommAlgebraEquiv→CommAlgebraHom : {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''}
                                  → CommAlgebraEquiv A B → CommAlgebraHom A B
  CommAlgebraEquiv→CommAlgebraHom (e , eIsHom) = e .fst , eIsHom

  CommAlgebraHom→CommRingHom : (A : CommAlgebra R ℓ') (B : CommAlgebra R ℓ'')
                              → CommAlgebraHom A B
                              → CommRingHom (CommAlgebra→CommRing A) (CommAlgebra→CommRing B)
  fst (CommAlgebraHom→CommRingHom A B f) = fst f
  IsCommRingHom.pres0 (snd (CommAlgebraHom→CommRingHom A B f)) = IsAlgebraHom.pres0 (snd f)
  IsCommRingHom.pres1 (snd (CommAlgebraHom→CommRingHom A B f)) = IsAlgebraHom.pres1 (snd f)
  IsCommRingHom.pres+ (snd (CommAlgebraHom→CommRingHom A B f)) = IsAlgebraHom.pres+ (snd f)
  IsCommRingHom.pres· (snd (CommAlgebraHom→CommRingHom A B f)) = IsAlgebraHom.pres· (snd f)
  IsCommRingHom.pres- (snd (CommAlgebraHom→CommRingHom A B f)) = IsAlgebraHom.pres- (snd f)

  module _ {M : CommAlgebra R ℓ'} {N : CommAlgebra R ℓ''} where
    open CommAlgebraStr {{...}}
    open IsAlgebraHom
    private
      instance
        _ = snd M
        _ = snd N

    makeCommAlgebraHom : (f : fst M → fst N)
                           → (fPres1 : f 1a ≡ 1a)
                           → (fPres+ : (x y : fst M) → f (x + y) ≡ f x + f y)
                           → (fPres· : (x y : fst M) → f (x · y) ≡ f x · f y)
                           → (fPres⋆ : (r : fst R) (x : fst M) → f (r ⋆ x) ≡ r ⋆ f x)
                           → CommAlgebraHom M N
    makeCommAlgebraHom f fPres1 fPres+ fPres· fPres⋆ = f , isHom
      where fPres0 =
                    f 0a                  ≡⟨ sym (+IdR _) ⟩
                    f 0a + 0a             ≡⟨ cong (λ u → f 0a + u) (sym (+InvR (f 0a))) ⟩
                    f 0a + (f 0a - f 0a)  ≡⟨ +Assoc (f 0a) (f 0a) (- f 0a) ⟩
                    (f 0a + f 0a) - f 0a  ≡⟨ cong (λ u → u - f 0a) (sym (fPres+ 0a 0a)) ⟩
                    f (0a + 0a) - f 0a    ≡⟨ cong (λ u → f u - f 0a) (+IdL 0a) ⟩
                    f 0a - f 0a           ≡⟨ +InvR (f 0a) ⟩
                    0a ∎

            isHom : IsCommAlgebraHom (snd M) f (snd N)
            pres0 isHom = fPres0
            pres1 isHom = fPres1
            pres+ isHom = fPres+
            pres· isHom = fPres·
            pres- isHom = (λ x →
                               f (- x) ≡⟨ sym (+IdR _) ⟩
                               (f (- x) + 0a) ≡⟨ cong (λ u → f (- x) + u) (sym (+InvR (f x))) ⟩
                               (f (- x) + (f x - f x)) ≡⟨ +Assoc _ _ _ ⟩
                               ((f (- x) + f x) - f x) ≡⟨ cong (λ u → u - f x) (sym (fPres+ _ _)) ⟩
                               (f ((- x) + x) - f x) ≡⟨ cong (λ u → f u - f x) (+InvL x) ⟩
                               (f 0a - f x) ≡⟨ cong (λ u → u - f x) fPres0 ⟩
                               (0a - f x) ≡⟨ +IdL _ ⟩ (- f x) ∎)
            pres⋆ isHom = fPres⋆

    isPropIsCommAlgebraHom : (f : fst M → fst N) → isProp (IsCommAlgebraHom (snd M) f (snd N))
    isPropIsCommAlgebraHom f = isPropIsAlgebraHom
                                 (CommRing→Ring R)
                                 (snd (CommAlgebra→Algebra M))
                                 f
                                 (snd (CommAlgebra→Algebra N))

isPropIsCommAlgebra : (R : CommRing ℓ) {A : Type ℓ'}
  (0a 1a : A)
  (_+_ _·_ : A → A → A)
  (-_ : A → A)
  (_⋆_ : ⟨ R ⟩ → A → A)
  → isProp (IsCommAlgebra R 0a 1a _+_ _·_ -_ _⋆_)
isPropIsCommAlgebra R _ _ _ _ _ _ =
  isOfHLevelRetractFromIso  IsCommAlgebraIsoΣ
    (isPropΣ (isPropIsAlgebra _ _ _ _ _ _ _)
      (λ alg → isPropΠ2 λ _ _ → alg .IsAlgebra.is-set _ _))

𝒮ᴰ-CommAlgebra : (R : CommRing ℓ) → DUARel (𝒮-Univ ℓ') (CommAlgebraStr R) (ℓ-max ℓ ℓ')
𝒮ᴰ-CommAlgebra {ℓ' = ℓ'} R =
  𝒮ᴰ-Record (𝒮-Univ _) (IsCommAlgebraEquiv {R = R})
    (fields:
      data[ 0a ∣ nul ∣ pres0 ]
      data[ 1a ∣ nul ∣ pres1 ]
      data[ _+_ ∣ bin ∣ pres+ ]
      data[ _·_ ∣ bin ∣ pres· ]
      data[ -_ ∣ autoDUARel _ _ ∣ pres- ]
      data[ _⋆_ ∣ autoDUARel _ _ ∣ pres⋆ ]
      prop[ isCommAlgebra ∣ (λ A ΣA
                               → isPropIsCommAlgebra
                                 {ℓ' = ℓ'}
                                 R
                                 (snd (fst (fst (fst (fst (fst ΣA))))))
                                 (snd (fst (fst (fst (fst ΣA)))))
                                 (snd (fst (fst (fst ΣA))))
                                 (snd (fst (fst ΣA)))
                                 (snd (fst ΣA))
                                 (snd ΣA)) ])
  where
  open CommAlgebraStr
  open IsAlgebraHom

  -- faster with some sharing
  nul = autoDUARel (𝒮-Univ _) (λ A → A)
  bin = autoDUARel (𝒮-Univ _) (λ A → A → A → A)

CommAlgebraPath : (R : CommRing ℓ) → (A B : CommAlgebra R ℓ') → (CommAlgebraEquiv A B) ≃ (A ≡ B)
CommAlgebraPath R = ∫ (𝒮ᴰ-CommAlgebra R) .UARel.ua

uaCommAlgebra : {R : CommRing ℓ} {A B : CommAlgebra R ℓ'} → CommAlgebraEquiv A B → A ≡ B
uaCommAlgebra {R = R} {A = A} {B = B} = equivFun (CommAlgebraPath R A B)

isGroupoidCommAlgebra : {R : CommRing ℓ} → isGroupoid (CommAlgebra R ℓ')
isGroupoidCommAlgebra A B = isOfHLevelRespectEquiv  (CommAlgebraPath _ _ _) (isSetAlgebraEquiv _ _)