------------------------------------------------------------------------
-- The Agda standard library
--
-- For each `IsX` algebraic structure `S`, lift the structure to the
-- 'pointwise' function space `A → S`: categorically, this is the
-- *power* object in the relevant category of `X` objects and morphisms
--
-- NB the module is parametrised only wrt `A`
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Algebra.Construct.Pointwise {a} (A : Set a) where

open import Algebra.Bundles
open import Algebra.Core using (Op₁; Op₂)
open import Algebra.Structures
open import Data.Product.Base using (_,_)
open import Function.Base using (id; _∘′_; const)
open import Level
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Structures using (IsEquivalence)

private

  variable
    c ℓ : Level
    C : Set c
    _≈_ : Rel C ℓ
    ε 0# 1# : C
    _⁻¹ -_ _⋆ : Op₁ C
    _∙_ _+_ _*_ : Op₂ C

  lift₀ : C → A → C
  lift₀ = const

  lift₁ : Op₁ C → Op₁ (A → C)
  lift₁ = _∘′_

  lift₂ : Op₂ C → Op₂ (A → C)
  lift₂ _∙_ g h x = (g x) ∙ (h x)

  liftRel : Rel C ℓ → Rel (A → C) (a ⊔ ℓ)
  liftRel _≈_ g h = ∀ x → (g x) ≈ (h x)


------------------------------------------------------------------------
-- Setoid structure: here rather than elsewhere? (could be imported?)

isEquivalence : IsEquivalence _≈_ → IsEquivalence (liftRel _≈_)
isEquivalence isEquivalence = record
  { refl = λ {f} _ → refl {f _}
  ; sym = λ f≈g _ → sym (f≈g _)
  ; trans = λ f≈g g≈h _ → trans (f≈g _) (g≈h _)
  }
  where open IsEquivalence isEquivalence

------------------------------------------------------------------------
-- Structures

isMagma : IsMagma _≈_ _∙_ → IsMagma (liftRel _≈_) (lift₂ _∙_)
isMagma isMagma = record
  { isEquivalence = isEquivalence M.isEquivalence
  ; ∙-cong = λ g h _ → M.∙-cong (g _) (h _)
  }
  where module M = IsMagma isMagma

isSemigroup : IsSemigroup _≈_ _∙_ → IsSemigroup (liftRel _≈_) (lift₂ _∙_)
isSemigroup isSemigroup = record
  { isMagma = isMagma M.isMagma
  ; assoc = λ f g h _ → M.assoc (f _) (g _) (h _)
  }
  where module M = IsSemigroup isSemigroup

isBand : IsBand _≈_ _∙_ → IsBand (liftRel _≈_) (lift₂ _∙_)
isBand isBand = record
  { isSemigroup = isSemigroup M.isSemigroup
  ; idem = λ f _ → M.idem (f _)
  }
  where module M = IsBand isBand

isCommutativeSemigroup : IsCommutativeSemigroup _≈_ _∙_ →
                         IsCommutativeSemigroup (liftRel _≈_) (lift₂ _∙_)
isCommutativeSemigroup isCommutativeSemigroup = record
  { isSemigroup = isSemigroup M.isSemigroup
  ; comm = λ f g _ → M.comm (f _) (g _)
  }
  where module M = IsCommutativeSemigroup isCommutativeSemigroup

isMonoid : IsMonoid _≈_ _∙_ ε → IsMonoid (liftRel _≈_) (lift₂ _∙_) (lift₀ ε)
isMonoid isMonoid = record
  { isSemigroup = isSemigroup M.isSemigroup
  ; identity = (λ f _ → M.identityˡ (f _)) , λ f _ → M.identityʳ (f _)
  }
  where module M = IsMonoid isMonoid

isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε →
                      IsCommutativeMonoid (liftRel _≈_) (lift₂ _∙_) (lift₀ ε)
isCommutativeMonoid isCommutativeMonoid = record
  { isMonoid = isMonoid M.isMonoid
  ; comm = λ f g _ → M.comm (f _) (g _)
  }
  where module M = IsCommutativeMonoid isCommutativeMonoid

isGroup : IsGroup _≈_ _∙_ ε _⁻¹ →
          IsGroup (liftRel _≈_) (lift₂ _∙_) (lift₀ ε) (lift₁ _⁻¹)
isGroup isGroup = record
  { isMonoid = isMonoid M.isMonoid
  ; inverse = (λ f _ → M.inverseˡ (f _)) , λ f _ → M.inverseʳ (f _)
  ; ⁻¹-cong = λ f _ → M.⁻¹-cong (f _)
  }
  where module M = IsGroup isGroup

isAbelianGroup : IsAbelianGroup _≈_ _∙_ ε _⁻¹ →
                 IsAbelianGroup (liftRel _≈_) (lift₂ _∙_) (lift₀ ε) (lift₁ _⁻¹)
isAbelianGroup isAbelianGroup = record
  { isGroup = isGroup M.isGroup
  ; comm = λ f g _ → M.comm (f _) (g _)
  }
  where module M = IsAbelianGroup isAbelianGroup

isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# →
             IsNearSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isNearSemiring isNearSemiring = record
  { +-isMonoid = isMonoid M.+-isMonoid
  ; *-cong =  λ g h _ → M.*-cong (g _) (h _)
  ; *-assoc =  λ f g h _ → M.*-assoc (f _) (g _) (h _)
  ; distribʳ = λ f g h _ → M.distribʳ (f _) (g _) (h _)
  ; zeroˡ = λ f _ → M.zeroˡ (f _)
  }
  where module M = IsNearSemiring isNearSemiring

isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _+_ _*_ 0# →
  IsSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isSemiringWithoutOne isSemiringWithoutOne = record
  { +-isCommutativeMonoid = isCommutativeMonoid M.+-isCommutativeMonoid
  ; *-cong =  λ g h _ → M.*-cong (g _) (h _)
  ; *-assoc =  λ f g h _ → M.*-assoc (f _) (g _) (h _)
  ; distrib = (λ f g h _ → M.distribˡ (f _) (g _) (h _)) , (λ f g h _ → M.distribʳ (f _) (g _) (h _))
  ; zero = (λ f _ → M.zeroˡ (f _)) , (λ f _ → M.zeroʳ (f _))
  }
  where module M = IsSemiringWithoutOne isSemiringWithoutOne

isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne _≈_ _+_ _*_ 0# →
  IsCommutativeSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#)
isCommutativeSemiringWithoutOne isCommutativeSemiringWithoutOne = record
  { isSemiringWithoutOne = isSemiringWithoutOne M.isSemiringWithoutOne
  ; *-comm = λ f g _ → M.*-comm (f _) (g _)
  }
  where module M = IsCommutativeSemiringWithoutOne isCommutativeSemiringWithoutOne

isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _≈_ _+_ _*_ 0# 1# →
  IsSemiringWithoutAnnihilatingZero (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isSemiringWithoutAnnihilatingZero isSemiringWithoutAnnihilatingZero = record
  { +-isCommutativeMonoid = isCommutativeMonoid M.+-isCommutativeMonoid
  ; *-cong =  λ g h _ → M.*-cong (g _) (h _)
  ; *-assoc =  λ f g h _ → M.*-assoc (f _) (g _) (h _)
  ; *-identity = (λ f _ → M.*-identityˡ (f _)) , λ f _ → M.*-identityʳ (f _)
  ; distrib = (λ f g h _ → M.distribˡ (f _) (g _) (h _)) , λ f g h _ → M.distribʳ (f _) (g _) (h _)
  }
  where module M = IsSemiringWithoutAnnihilatingZero isSemiringWithoutAnnihilatingZero

isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1# →
             IsSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isSemiring isSemiring = record
  { isSemiringWithoutAnnihilatingZero = isSemiringWithoutAnnihilatingZero M.isSemiringWithoutAnnihilatingZero
  ; zero = (λ f _ → M.zeroˡ (f _)) , λ f _ → M.zeroʳ (f _)
  }
  where module M = IsSemiring isSemiring

isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1# →
  IsCommutativeSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isCommutativeSemiring isCommutativeSemiring = record
  { isSemiring = isSemiring M.isSemiring
  ; *-comm = λ f g _ → M.*-comm (f _) (g _)
  }
  where module M = IsCommutativeSemiring isCommutativeSemiring

isIdempotentSemiring : IsIdempotentSemiring _≈_ _+_ _*_ 0# 1# →
  IsIdempotentSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isIdempotentSemiring isIdempotentSemiring = record
  { isSemiring = isSemiring M.isSemiring
  ; +-idem = λ f _ → M.+-idem (f _)
  }
  where module M = IsIdempotentSemiring isIdempotentSemiring

isKleeneAlgebra : IsKleeneAlgebra _≈_ _+_ _*_ _⋆ 0# 1# →
  IsKleeneAlgebra (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ _⋆) (lift₀ 0#) (lift₀ 1#)
isKleeneAlgebra isKleeneAlgebra = record
  { isIdempotentSemiring = isIdempotentSemiring M.isIdempotentSemiring
  ; starExpansive = (λ f _ → M.starExpansiveˡ (f _)) , λ f _ → M.starExpansiveʳ (f _)
  ; starDestructive = (λ f g h i _ → M.starDestructiveˡ (f _) (g _) (h _) (i _))
                    , (λ f g h i _ → M.starDestructiveʳ (f _) (g _) (h _) (i _))
  }
  where module M = IsKleeneAlgebra isKleeneAlgebra

isQuasiring : IsQuasiring _≈_ _+_ _*_ 0# 1# →
  IsQuasiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#)
isQuasiring isQuasiring = record
  { +-isMonoid = isMonoid M.+-isMonoid
  ; *-cong =  λ g h _ → M.*-cong (g _) (h _)
  ; *-assoc =  λ f g h _ → M.*-assoc (f _) (g _) (h _)
  ; *-identity = (λ f _ → M.*-identityˡ (f _)) , λ f _ → M.*-identityʳ (f _)
  ; distrib = (λ f g h _ → M.distribˡ (f _) (g _) (h _)) , λ f g h _ → M.distribʳ (f _) (g _) (h _)
  ; zero = (λ f _ → M.zeroˡ (f _)) , λ f _ → M.zeroʳ (f _)
  }
  where module M = IsQuasiring isQuasiring

isRing : IsRing _≈_ _+_ _*_ -_ 0# 1# →
         IsRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#)
isRing isRing = record
  { +-isAbelianGroup = isAbelianGroup M.+-isAbelianGroup
  ; *-cong = λ g h _ → M.*-cong (g _) (h _)
  ; *-assoc = λ f g h _ → M.*-assoc (f _) (g _) (h _)
  ; *-identity = (λ f _ → M.*-identityˡ (f _)) , λ f _ → M.*-identityʳ (f _)
  ; distrib = (λ f g h _ → M.distribˡ (f _) (g _) (h _)) , λ f g h _ → M.distribʳ (f _) (g _) (h _)
  }
  where module M = IsRing isRing

isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1# →
    IsCommutativeRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#)
isCommutativeRing isCommutativeRing = record
  { isRing = isRing M.isRing
  ; *-comm = λ f g _ → M.*-comm (f _) (g _)
  }
  where module M = IsCommutativeRing isCommutativeRing

------------------------------------------------------------------------
-- Bundles

magma : Magma c ℓ → Magma (a ⊔ c) (a ⊔ ℓ)
magma m = record { isMagma = isMagma (Magma.isMagma m) }

semigroup : Semigroup c ℓ → Semigroup (a ⊔ c) (a ⊔ ℓ)
semigroup m = record { isSemigroup = isSemigroup (Semigroup.isSemigroup m) }

band : Band c ℓ → Band (a ⊔ c) (a ⊔ ℓ)
band m = record { isBand = isBand (Band.isBand m) }

commutativeSemigroup : CommutativeSemigroup c ℓ → CommutativeSemigroup (a ⊔ c) (a ⊔ ℓ)
commutativeSemigroup m = record { isCommutativeSemigroup = isCommutativeSemigroup (CommutativeSemigroup.isCommutativeSemigroup m) }

monoid : Monoid c ℓ → Monoid (a ⊔ c) (a ⊔ ℓ)
monoid m = record { isMonoid = isMonoid (Monoid.isMonoid m) }

commutativeMonoid : CommutativeMonoid c ℓ → CommutativeMonoid (a ⊔ c) (a ⊔ ℓ)
commutativeMonoid m = record { isCommutativeMonoid = isCommutativeMonoid (CommutativeMonoid.isCommutativeMonoid m) }

group : Group c ℓ → Group (a ⊔ c) (a ⊔ ℓ)
group m = record { isGroup = isGroup (Group.isGroup m) }

abelianGroup : AbelianGroup c ℓ → AbelianGroup (a ⊔ c) (a ⊔ ℓ)
abelianGroup m = record { isAbelianGroup = isAbelianGroup (AbelianGroup.isAbelianGroup m) }

nearSemiring : NearSemiring c ℓ → NearSemiring (a ⊔ c) (a ⊔ ℓ)
nearSemiring m = record { isNearSemiring = isNearSemiring (NearSemiring.isNearSemiring m) }

semiringWithoutOne : SemiringWithoutOne c ℓ → SemiringWithoutOne (a ⊔ c) (a ⊔ ℓ)
semiringWithoutOne m = record { isSemiringWithoutOne = isSemiringWithoutOne (SemiringWithoutOne.isSemiringWithoutOne m) }

commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne c ℓ → CommutativeSemiringWithoutOne (a ⊔ c) (a ⊔ ℓ)
commutativeSemiringWithoutOne m = record
  { isCommutativeSemiringWithoutOne = isCommutativeSemiringWithoutOne (CommutativeSemiringWithoutOne.isCommutativeSemiringWithoutOne m) }

semiring : Semiring c ℓ → Semiring (a ⊔ c) (a ⊔ ℓ)
semiring m = record { isSemiring = isSemiring (Semiring.isSemiring m) }

commutativeSemiring : CommutativeSemiring c ℓ → CommutativeSemiring (a ⊔ c) (a ⊔ ℓ)
commutativeSemiring m = record { isCommutativeSemiring = isCommutativeSemiring (CommutativeSemiring.isCommutativeSemiring m) }

idempotentSemiring : IdempotentSemiring c ℓ → IdempotentSemiring (a ⊔ c) (a ⊔ ℓ)
idempotentSemiring m = record { isIdempotentSemiring = isIdempotentSemiring (IdempotentSemiring.isIdempotentSemiring m) }

kleeneAlgebra : KleeneAlgebra c ℓ → KleeneAlgebra (a ⊔ c) (a ⊔ ℓ)
kleeneAlgebra m = record { isKleeneAlgebra = isKleeneAlgebra (KleeneAlgebra.isKleeneAlgebra m) }

quasiring : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ)
quasiring m = record { isQuasiring = isQuasiring (Quasiring.isQuasiring m) }

ring : Ring c ℓ → Ring (a ⊔ c) (a ⊔ ℓ)
ring m = record { isRing = isRing (Ring.isRing m) }

commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
commutativeRing m = record { isCommutativeRing = isCommutativeRing (CommutativeRing.isCommutativeRing m) }