From 3cf9d5a4ae5d49d6e4b470e3a90068b9f2e7a108 Mon Sep 17 00:00:00 2001 From: e-mniang Date: Thu, 28 Aug 2025 13:39:26 -0400 Subject: [PATCH 1/4] update of pr 1945 --- src/Data/Vec/Functional/Algebra/Base.agda | 142 ++++ .../Vec/Functional/Algebra/Properties.agda | 734 ++++++++++++++++++ 2 files changed, 876 insertions(+) create mode 100644 src/Data/Vec/Functional/Algebra/Base.agda create mode 100644 src/Data/Vec/Functional/Algebra/Properties.agda diff --git a/src/Data/Vec/Functional/Algebra/Base.agda b/src/Data/Vec/Functional/Algebra/Base.agda new file mode 100644 index 0000000000..e79c001267 --- /dev/null +++ b/src/Data/Vec/Functional/Algebra/Base.agda @@ -0,0 +1,142 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Some Vector-related module Definitions +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.Vec.Functional.Algebra.Base where + +open import Level using (Level; suc; _⊔_) +open import Function using (_$_) +open import Data.Nat using (ℕ) +open import Data.Fin using (Fin) +open import Data.Vec.Functional +open import Algebra.Core +open import Algebra.Bundles +open import Algebra.Module +open import Relation.Binary using (Rel) +open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise) + +private variable + a ℓ : Level + A : Set ℓ + n : ℕ + +-- Vector relation lifting +VecRel : {A : Set a} → Rel A ℓ → Rel (Vector A n) ℓ +VecRel _≈_ xs ys = Pointwise _≈_ xs ys + +-- Binary operation lifting +lift₂ᴹ : {A : Set a} → Op₂ A → Op₂ (Vector A n) +lift₂ᴹ _∙_ = zipWith _∙_ + +-- Unary operation lifting +lift₁ᴹ : {A : Set a} → Op₁ A → Op₁ (Vector A n) +lift₁ᴹ f = map f + +-- Vector RawMagma construction +VecRawMagma : RawMagma a ℓ → (n : ℕ) → RawMagma a ℓ +VecRawMagma M n = + record + { Carrier = Vector M.Carrier n + ; _≈_ = VecRel M._≈_ + ; _∙_ = lift₂ᴹ M._∙_ + } + where module M = RawMagma M + +-- Vector RawMonoid construction +VecRawMonoid : RawMonoid a ℓ → (n : ℕ) → RawMonoid a ℓ +VecRawMonoid M n = + record + { RawMagma (VecRawMagma M.rawMagma n) + ; ε = λ _ → M.ε + } + where + module M = RawMonoid M + +-- Vector RawGroup construction +VecRawGroup : RawGroup a ℓ → (n : ℕ) → RawGroup a ℓ +VecRawGroup G n = + record + { RawMonoid (VecRawMonoid G.rawMonoid n) + ; _⁻¹ = lift₁ᴹ G._⁻¹ + } + where module G = RawGroup G + +-- Vector RawNearSemiring construction +VecRawNearSemiring : RawNearSemiring a ℓ → (n : ℕ) → RawNearSemiring a ℓ +VecRawNearSemiring NS n = + record + { Carrier = Vector NS.Carrier n + ; _≈_ = VecRel NS._≈_ + ; _+_ = lift₂ᴹ NS._+_ + ; _*_ = lift₂ᴹ NS._*_ + ; 0# = λ _ → NS.0# + } + where module NS = RawNearSemiring NS + +-- Vector RawSemiring construction +VecRawSemiring : RawSemiring a ℓ → (n : ℕ) → RawSemiring a ℓ +VecRawSemiring S n = + record + { RawNearSemiring (VecRawNearSemiring S.rawNearSemiring n) + ; 1# = λ _ → S.1# + } + where module S = RawSemiring S + +-- Vector RawRing construction +VecRawRing : RawRing a ℓ → (n : ℕ) → RawRing a ℓ +VecRawRing R n = + record + { RawSemiring (VecRawSemiring R.rawSemiring n) + ; -_ = lift₁ᴹ R.-_ + } + where module R = RawRing R + + + +-- Left scalar action obtained from the ring/semiring multiplication +_*ₗ_ : {S : Set a} → Op₂ S → Opₗ S (Vector S n) +_*ₗ_ _*_ r xs = map (λ x → _*_ r x) xs + +-- Right scalar action (same underlying Op₂, but as a right action) +_*ᵣ_ : {S : Set a} → Op₂ S → Opᵣ S (Vector S n) +_*ᵣ_ _*_ xs r = map (λ x → _*_ x r) xs + + +VecRawLeftSemimodule : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawLeftSemimodule (RawNearSemiring.Carrier NS) a ℓ +VecRawLeftSemimodule NS n = + record + { Carrierᴹ = Vector NS.Carrier n + ; _≈ᴹ_ = VecRel NS._≈_ + ; _+ᴹ_ = lift₂ᴹ NS._+_ + ; _*ₗ_ = _*ₗ_ NS._*_ + ; 0ᴹ = λ _ → NS.0# + } + where module NS = RawNearSemiring NS + +VecRawRightSemimodule : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawRightSemimodule (RawNearSemiring.Carrier NS) a ℓ +VecRawRightSemimodule NS n = + record + { Carrierᴹ = Vector NS.Carrier n + ; _≈ᴹ_ = VecRel NS._≈_ + ; _+ᴹ_ = lift₂ᴹ NS._+_ + ; _*ᵣ_ = _*ᵣ_ NS._*_ + ; 0ᴹ = λ _ → NS.0# + } + where module NS = RawNearSemiring NS + +VecRawBisemimodule : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawBisemimodule (RawNearSemiring.Carrier NS) + (RawNearSemiring.Carrier NS) a ℓ +VecRawBisemimodule NS n = + record + { Carrierᴹ = Vector NS.Carrier n + ; _≈ᴹ_ = VecRel NS._≈_ + ; _+ᴹ_ = lift₂ᴹ NS._+_ + ; _*ₗ_ = _*ₗ_ NS._*_ + ; _*ᵣ_ = _*ᵣ_ NS._*_ + ; 0ᴹ = λ _ → NS.0# + } + where module NS = RawNearSemiring NS diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda new file mode 100644 index 0000000000..b88b95f1f7 --- /dev/null +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -0,0 +1,734 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties for the functional vector algebra approach +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.Vec.Functional.Algebra.Properties where + +open import Level using (Level; _⊔_) +open import Function using (_$_; flip) +open import Data.Product hiding (map) +open import Data.Nat using (ℕ) +open import Data.Fin using (Fin; zero; suc) +open import Data.Vec.Functional +open import Algebra.Core +open import Algebra.Bundles +open import Algebra.Module +open import Algebra.Module.Structures +open import Relation.Binary +import Algebra.Definitions as ADefinitions +open import Algebra.Structures +open import Data.Vec.Functional.Algebra.Base +import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as Pointwise + +private variable + a ℓ : Level + A : Set ℓ + n : ℕ + +------------------------------------------------------------------------ +-- Raw structure properties + +module RawMagmaProperties (rawMagma : RawMagma a ℓ) (n : ℕ) where + private + vecMagma = VecRawMagma rawMagma n + module VM = RawMagma vecMagma + module M = RawMagma rawMagma + + open IsEquivalence + + isMagma : IsMagma M._≈_ M._∙_ → IsMagma VM._≈_ VM._∙_ + isMagma base = record + { isEquivalence = flip Pointwise.isEquivalence _ B.isEquivalence + ; ∙-cong = λ x≈y u≈v i → B.∙-cong (x≈y i) (u≈v i) + } + where module B = IsMagma base + + isCommutativeMagma : IsCommutativeMagma M._≈_ M._∙_ → IsCommutativeMagma VM._≈_ VM._∙_ + isCommutativeMagma base = record + { isMagma = isMagma CM.isMagma + ; comm = λ xs ys i → CM.comm (xs i) (ys i) + } + where module CM = IsCommutativeMagma base + + isSemigroup : IsSemigroup M._≈_ M._∙_ → IsSemigroup VM._≈_ VM._∙_ + isSemigroup base = record + { isMagma = isMagma SG.isMagma + ; assoc = λ xs ys zs i → SG.assoc (xs i) (ys i) (zs i) + } + where module SG = IsSemigroup base + + isCommutativeSemigroup : IsCommutativeSemigroup M._≈_ M._∙_ → IsCommutativeSemigroup VM._≈_ VM._∙_ + isCommutativeSemigroup base = record + { isSemigroup = isSemigroup CS.isSemigroup + ; comm = λ xs ys i → CS.comm (xs i) (ys i) + } + where module CS = IsCommutativeSemigroup base + +------------------------------------------------------------------------ + +module RawMonoidProperties (rawMonoid : RawMonoid a ℓ) (n : ℕ) where + private + vecMonoid = VecRawMonoid rawMonoid n + module VM = RawMonoid vecMonoid + module RM = RawMonoid rawMonoid + + open RawMagmaProperties (RawMonoid.rawMagma rawMonoid) n public + + private + module ≈ = ADefinitions RM._≈_ + module ≈ᴹ = ADefinitions VM._≈_ + + +ᴹ-identityˡ : ≈.LeftIdentity RM.ε RM._∙_ → ≈ᴹ.LeftIdentity VM.ε VM._∙_ + +ᴹ-identityˡ idˡ xs i = idˡ (xs i) + + +ᴹ-identityʳ : ≈.RightIdentity RM.ε RM._∙_ → ≈ᴹ.RightIdentity VM.ε VM._∙_ + +ᴹ-identityʳ idʳ xs i = idʳ (xs i) + + +ᴹ-identity : ≈.Identity RM.ε RM._∙_ → ≈ᴹ.Identity VM.ε VM._∙_ + +ᴹ-identity (idˡ , idʳ) = +ᴹ-identityˡ idˡ , +ᴹ-identityʳ idʳ + + isMonoid : IsMonoid RM._≈_ RM._∙_ RM.ε → IsMonoid VM._≈_ VM._∙_ VM.ε + isMonoid isMonoid = record + { isSemigroup = isSemigroup M.isSemigroup + ; identity = +ᴹ-identity M.identity + } where module M = IsMonoid isMonoid + + isCommutativeMonoid : IsCommutativeMonoid RM._≈_ RM._∙_ RM.ε → IsCommutativeMonoid VM._≈_ VM._∙_ VM.ε + isCommutativeMonoid base = record + { isMonoid = isMonoid CM.isMonoid + ; comm = λ xs ys i → CM.comm (xs i) (ys i) + } where module CM = IsCommutativeMonoid base + +------------------------------------------------------------------------ + +module RawGroupProperties (rawGroup : RawGroup a ℓ) (n : ℕ) where + private + vecGroup = VecRawGroup rawGroup n + module RG = RawGroup vecGroup + module G = RawGroup rawGroup + open RawMonoidProperties (RawGroup.rawMonoid rawGroup) n public + + private + module ≈ = ADefinitions G._≈_ + module ≈ᴹ = ADefinitions RG._≈_ + + -ᴹ‿inverseˡ : ≈.LeftInverse G.ε G._⁻¹ G._∙_ → ≈ᴹ.LeftInverse RG.ε RG._⁻¹ RG._∙_ + -ᴹ‿inverseˡ -‿inverseˡ xs i = -‿inverseˡ (xs i) + + -ᴹ‿inverseʳ : ≈.RightInverse G.ε G._⁻¹ G._∙_ → ≈ᴹ.RightInverse RG.ε RG._⁻¹ RG._∙_ + -ᴹ‿inverseʳ -‿inverseʳ xs i = -‿inverseʳ (xs i) + + -ᴹ‿inverse : ≈.Inverse G.ε G._⁻¹ G._∙_ → ≈ᴹ.Inverse RG.ε RG._⁻¹ RG._∙_ + -ᴹ‿inverse (-‿inverseˡ , -‿inverseʳ) = -ᴹ‿inverseˡ -‿inverseˡ , -ᴹ‿inverseʳ -‿inverseʳ + + -ᴹ‿cong : ≈.Congruent₁ G._⁻¹ → ≈ᴹ.Congruent₁ RG._⁻¹ + -ᴹ‿cong -‿cong xs≈ys i = -‿cong (xs≈ys i) + + isGroup : IsGroup G._≈_ G._∙_ G.ε G._⁻¹ → IsGroup RG._≈_ RG._∙_ RG.ε RG._⁻¹ + isGroup isGroup = record + { isMonoid = isMonoid M.isMonoid + ; inverse = -ᴹ‿inverse M.inverse + ; ⁻¹-cong = -ᴹ‿cong M.⁻¹-cong + } where module M = IsGroup isGroup + + isAbelianGroup : IsAbelianGroup G._≈_ G._∙_ G.ε G._⁻¹ → IsAbelianGroup RG._≈_ RG._∙_ RG.ε RG._⁻¹ + isAbelianGroup base = record + { isGroup = isGroup AG.isGroup + ; comm = λ xs ys i → AG.comm (xs i) (ys i) + } + where module AG = IsAbelianGroup base + +------------------------------------------------------------------------ + +module VecSemiringProperties (rawSemiring : RawSemiring a ℓ) (n : ℕ) where + private + module SR = RawSemiring rawSemiring + rawNearSemiring = SR.rawNearSemiring + module NS = RawNearSemiring rawNearSemiring + vecNearSemiring = VecRawNearSemiring rawNearSemiring n + vecSemiring = VecRawSemiring rawSemiring n + module RNS = RawNearSemiring vecNearSemiring + module RS = RawSemiring vecSemiring + vecLeftSemi = VecRawLeftSemimodule rawNearSemiring n + vecRightSemi = VecRawRightSemimodule rawNearSemiring n + module LSM = RawLeftSemimodule vecLeftSemi + module RSM = RawRightSemimodule vecRightSemi + + open RawMonoidProperties (RawSemiring.*-rawMonoid rawSemiring) n public + using () + renaming (+ᴹ-identity to *ᴹ-identity) + + private + module ≈ = ADefinitions NS._≈_ + module LD = LeftDefs NS.Carrier RNS._≈_ + module RD = RightDefs NS.Carrier RNS._≈_ + + *ₗ-identityˡ : ≈.LeftIdentity SR.1# NS._*_ → LD.LeftIdentity SR.1# (λ r xs → LSM._*ₗ_ r xs) + *ₗ-identityˡ *-idˡ xs i = *-idˡ (xs i) + + *ᵣ-identityʳ : ≈.RightIdentity SR.1# NS._*_ → RD.RightIdentity SR.1# (λ xs r → RSM._*ᵣ_ xs r) + *ᵣ-identityʳ *-idʳ xs i = *-idʳ (xs i) +------------------------------------------------------------------------ + +module RawNearSemiringProperties {ℓ ℓr} (R : Semiring ℓ ℓr) (n : ℕ) where + open Semiring R + private + module SR = RawSemiring rawSemiring + vecLeftSemi = VecRawLeftSemimodule rawNearSemiring n + vecRightSemi = VecRawRightSemimodule rawNearSemiring n + module LSM = RawLeftSemimodule vecLeftSemi + vecNearSemiring = VecRawNearSemiring rawNearSemiring n + module RNS = RawNearSemiring vecNearSemiring + module RSM = RawRightSemimodule vecRightSemi + module NS = RawNearSemiring rawNearSemiring + + open RawMonoidProperties +-rawMonoid + + isPreleftSemimoduleVec : IsPreleftSemimodule R RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ + isPreleftSemimoduleVec = record + { *ₗ-cong = λ x≈y u≈v i → *-cong x≈y (u≈v i) + ; *ₗ-zeroˡ = λ xs i → zeroˡ (xs i) + ; *ₗ-distribʳ = λ xs m n i → distribʳ (xs i) m n + ; *ₗ-identityˡ = λ xs i → *-identityˡ (xs i) + ; *ₗ-assoc = λ m n xs i → *-assoc m n (xs i) + ; *ₗ-zeroʳ = λ r i → zeroʳ r + ; *ₗ-distribˡ = λ m xs ys i → distribˡ m (xs i) (ys i) + } + + + isPrerightSemimoduleVec : IsPrerightSemimodule R RNS._≈_ RNS._+_ RNS.0# RSM._*ᵣ_ + isPrerightSemimoduleVec = record + { *ᵣ-cong = λ x≈y u≈v i → *-cong (x≈y i) u≈v + ; *ᵣ-zeroʳ = λ xs i → zeroʳ (xs i) + ; *ᵣ-distribˡ = λ xs m n i → distribˡ (xs i) m n + ; *ᵣ-identityʳ = λ xs i → *-identityʳ (xs i) + ; *ᵣ-assoc = λ xs m n i → *-assoc (xs i) m n + ; *ᵣ-zeroˡ = λ r i → zeroˡ r + ; *ᵣ-distribʳ = λ xs m n i → distribʳ xs (m i) (n i) + } + + isBisemimoduleVec : IsBisemimodule R R RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ RSM._*ᵣ_ + isBisemimoduleVec = record + { +ᴹ-isCommutativeMonoid = isCommutativeMonoid n +-isCommutativeMonoid + ; isPreleftSemimodule = isPreleftSemimoduleVec + ; isPrerightSemimodule = isPrerightSemimoduleVec + ; *ₗ-*ᵣ-assoc = λ xs m ys i → *-assoc xs (m i) ys + } + + private + module ≈ = ADefinitions NS._≈_ + module ≈ᴹ = ADefinitions RNS._≈_ + + vec1# : Vector NS.Carrier n + vec1# = λ _ → SR.1# + + isSemiringVec : IsSemiring RNS._≈_ RNS._+_ RNS._*_ RNS.0# vec1# + isSemiringVec = record { + isSemiringWithoutAnnihilatingZero = record + { +-isCommutativeMonoid = isCommutativeMonoid n +-isCommutativeMonoid + ; *-cong = λ x≈y u≈v i → *-cong (x≈y i) (u≈v i) + ; *-assoc = λ xs ys zs i → *-assoc (xs i) (ys i) (zs i) + ; *-identity = (λ xs i → *-identityˡ (xs i)) , (λ xs i → *-identityʳ (xs i)) + ; distrib = (λ xs ys zs i → distribˡ (xs i) (ys i) (zs i)) , + (λ xs ys zs i → distribʳ (xs i) (ys i) (zs i)) + } + ; zero = (λ xs i → zeroˡ (xs i)) , (λ xs i → zeroʳ (xs i)) } + +------------------------------------------------------------------------ + +module MagmaProperties (magma : Magma a ℓ) (n : ℕ) where + open Magma magma using (_≈_; _∙_; isMagma; rawMagma) + private + vecMagma = VecRawMagma rawMagma n + module VM = RawMagma vecMagma + module RM = RawMagma rawMagma + + open RawMagmaProperties rawMagma n public renaming + ( isMagma to vec-isMagma + ; isCommutativeMagma to vec-isCommutativeMagma + ; isSemigroup to vec-isSemigroup + ; isCommutativeSemigroup to vec-isCommutativeSemigroup + ) + + +ᴹ-isMagma : IsMagma VM._≈_ VM._∙_ + +ᴹ-isMagma = vec-isMagma isMagma + + +ᴹ-magma : Magma _ _ + +ᴹ-magma = record { isMagma = +ᴹ-isMagma } + +------------------------------------------------------------------------ + +module CommutativeMagmaProperties (commutativeMagma : CommutativeMagma a ℓ) (n : ℕ) where + open CommutativeMagma commutativeMagma + private + vecMagma = VecRawMagma rawMagma n + module VM = RawMagma vecMagma + module M = RawMagma rawMagma + + open MagmaProperties magma n public + + +ᴹ-isCommutativeMagma : IsCommutativeMagma VM._≈_ VM._∙_ + +ᴹ-isCommutativeMagma = vec-isCommutativeMagma isCommutativeMagma + + +ᴹ-commutativeMagma : CommutativeMagma _ _ + +ᴹ-commutativeMagma = record { isCommutativeMagma = +ᴹ-isCommutativeMagma } + +------------------------------------------------------------------------ + +module SemiRawGroupProperties (semigroup : Semigroup a ℓ) (n : ℕ) where + open Semigroup semigroup + + private + vecMagma = VecRawMagma rawMagma n + module VM = RawMagma vecMagma + module M = RawMagma rawMagma + + open MagmaProperties magma n public + + +ᴹ-isSemigroup : IsSemigroup VM._≈_ VM._∙_ + +ᴹ-isSemigroup = vec-isSemigroup isSemigroup + + +ᴹ-semigroup : Semigroup _ _ + +ᴹ-semigroup = record { isSemigroup = +ᴹ-isSemigroup } + +------------------------------------------------------------------------ + +module CommutativeSemigroupProperties (commutativeSemigroup : CommutativeSemigroup a ℓ) (n : ℕ) where + open CommutativeSemigroup commutativeSemigroup + + private + vecMagma = VecRawMagma rawMagma n + module VM = RawMagma vecMagma + module M = RawMagma rawMagma + + open MagmaProperties magma n public + + +ᴹ-isCommutativeSemigroup : IsCommutativeSemigroup VM._≈_ VM._∙_ + +ᴹ-isCommutativeSemigroup = vec-isCommutativeSemigroup isCommutativeSemigroup + + +ᴹ-commutativeSemigroup : CommutativeSemigroup _ _ + +ᴹ-commutativeSemigroup = record { isCommutativeSemigroup = +ᴹ-isCommutativeSemigroup } + +------------------------------------------------------------------------ + +module MonoidProperties (monoid : Monoid a ℓ) (n : ℕ) where + open Monoid monoid + private + vecMonoid = VecRawMonoid rawMonoid n + module VM = RawMonoid vecMonoid + module M = RawMonoid rawMonoid + + open RawMonoidProperties rawMonoid n public using (+ᴹ-identity) + open SemiRawGroupProperties semigroup n public + + +ᴹ-isMonoid : IsMonoid VM._≈_ VM._∙_ VM.ε + +ᴹ-isMonoid = record + { isSemigroup = +ᴹ-isSemigroup + ; identity = +ᴹ-identity identity + } + +------------------------------------------------------------------------ + +module CommutativeMonoidProperties (commutativeMonoid : CommutativeMonoid a ℓ) (n : ℕ) where + open CommutativeMonoid commutativeMonoid + + private + vecMonoid = VecRawMonoid rawMonoid n + module VM = RawMonoid vecMonoid + module M = RawMonoid rawMonoid + + open RawMonoidProperties rawMonoid n + using () + renaming ( isCommutativeMonoid to vec-isCommutativeMonoid ) + + +ᴹ-isCommutativeMonoid : IsCommutativeMonoid VM._≈_ VM._∙_ VM.ε + +ᴹ-isCommutativeMonoid = vec-isCommutativeMonoid isCommutativeMonoid + + +ᴹ-commutativeMonoid : CommutativeMonoid _ _ + +ᴹ-commutativeMonoid = record { isCommutativeMonoid = +ᴹ-isCommutativeMonoid } + +------------------------------------------------------------------------ + +module GroupProperties (group : Group a ℓ) (n : ℕ) where + open Group group + + private + vecGroup = VecRawGroup rawGroup n + module VG = RawGroup vecGroup + module G = RawGroup rawGroup + + open RawGroupProperties rawGroup n public using (-ᴹ‿inverse; -ᴹ‿cong) + open MonoidProperties monoid n public + + +ᴹ-isGroup : IsGroup VG._≈_ VG._∙_ VG.ε VG._⁻¹ + +ᴹ-isGroup = record + { isMonoid = +ᴹ-isMonoid + ; inverse = -ᴹ‿inverse inverse + ; ⁻¹-cong = -ᴹ‿cong ⁻¹-cong + } + + +ᴹ-group : Group _ _ + +ᴹ-group = record { isGroup = +ᴹ-isGroup } + +------------------------------------------------------------------------ + +module AbelianGroupProperties (abelianGroup : AbelianGroup a ℓ) (n : ℕ) where + open AbelianGroup abelianGroup + private + vecGroup = VecRawGroup rawGroup n + module VG = RawGroup vecGroup + + open GroupProperties group n public + + +ᴹ-isAbelianGroup : IsAbelianGroup VG._≈_ VG._∙_ VG.ε VG._⁻¹ + +ᴹ-isAbelianGroup = record + { isGroup = +ᴹ-isGroup + ; comm = λ xs ys i → comm (xs i) (ys i) + } + + +ᴹ-abelianGroup : AbelianGroup _ _ + +ᴹ-abelianGroup = record { isAbelianGroup = +ᴹ-isAbelianGroup } + +------------------------------------------------------------------------ + +module NearSemiringProperties (nearSemiring : NearSemiring a ℓ) (n : ℕ) where + open NearSemiring nearSemiring + private + module N = NearSemiring nearSemiring + vecNearSemiring = VecRawNearSemiring rawNearSemiring n + module RNS = RawNearSemiring vecNearSemiring + + open MonoidProperties +-monoid n public using (+ᴹ-isMonoid) + + +ᴹ-*-isNearSemiring : IsNearSemiring RNS._≈_ RNS._+_ RNS._*_ RNS.0# + +ᴹ-*-isNearSemiring = record + { +-isMonoid = +ᴹ-isMonoid + ; *-cong = λ x≈y u≈v i → N.*-cong (x≈y i) (u≈v i) + ; *-assoc = λ xs ys zs i → N.*-assoc (xs i) (ys i) (zs i) + ; distribʳ = λ xs ys zs i → N.distribʳ (xs i) (ys i) (zs i) + ; zeroˡ = λ xs i → N.zeroˡ (xs i) + } + + + +ᴹ-*-nearSemiring : NearSemiring _ _ + +ᴹ-*-nearSemiring = record { isNearSemiring = +ᴹ-*-isNearSemiring } + +------------------------------------------------------------------------ + +module SemiringWithoutOneProperties (semiringWithoutOne : SemiringWithoutOne a ℓ) (n : ℕ) where + open SemiringWithoutOne semiringWithoutOne + private + vecNearSemiring = VecRawNearSemiring rawNearSemiring n + module RNS = RawNearSemiring vecNearSemiring + module SWO = SemiringWithoutOne semiringWithoutOne + + open CommutativeMonoidProperties +-commutativeMonoid n public using (+ᴹ-isCommutativeMonoid) + + +ᴹ-*-isSemiringWithoutOne : IsSemiringWithoutOne RNS._≈_ RNS._+_ RNS._*_ RNS.0# + +ᴹ-*-isSemiringWithoutOne = record + { +-isCommutativeMonoid = +ᴹ-isCommutativeMonoid + ; *-cong = λ x≈y u≈v i → SWO.*-cong (x≈y i) (u≈v i) + ; *-assoc = λ xs ys zs i → SWO.*-assoc (xs i) (ys i) (zs i) + ; distrib = (λ xs ys zs i → proj₁ SWO.distrib (xs i) (ys i) (zs i)) , + (λ xs ys zs i → proj₂ SWO.distrib (xs i) (ys i) (zs i)) + ; zero = (λ xs i → proj₁ SWO.zero (xs i)) , + (λ xs i → proj₂ SWO.zero (xs i)) + } + + +ᴹ-*-semiringWithoutOne : SemiringWithoutOne _ _ + +ᴹ-*-semiringWithoutOne = record { isSemiringWithoutOne = +ᴹ-*-isSemiringWithoutOne } + +------------------------------------------------------------------------ + +module CommutativeSemiringWithoutOneProperties + (commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne a ℓ) (n : ℕ) where + + open CommutativeSemiringWithoutOne commutativeSemiringWithoutOne + private + module CSWO = CommutativeSemiringWithoutOne commutativeSemiringWithoutOne + vecNearSemiring = VecRawNearSemiring rawNearSemiring n + module RNS = RawNearSemiring vecNearSemiring + + open SemiringWithoutOneProperties semiringWithoutOne n public + + +ᴹ-*-isCommutativeSemiringWithoutOne + : IsCommutativeSemiringWithoutOne RNS._≈_ RNS._+_ RNS._*_ RNS.0# + +ᴹ-*-isCommutativeSemiringWithoutOne = record + { isSemiringWithoutOne = +ᴹ-*-isSemiringWithoutOne + ; *-comm = λ xs ys i → CSWO.*-comm (xs i) (ys i) + } + + +ᴹ-*-commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne _ _ + +ᴹ-*-commutativeSemiringWithoutOne = + record { isCommutativeSemiringWithoutOne = +ᴹ-*-isCommutativeSemiringWithoutOne } + +------------------------------------------------------------------------ + +module SemiringWithoutAnnihilatingZeroProperties + (semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ) + (n : ℕ) where + + open SemiringWithoutAnnihilatingZero semiringWithoutAnnihilatingZero + private + module SWAZ = SemiringWithoutAnnihilatingZero semiringWithoutAnnihilatingZero + + vecSemiring = VecRawSemiring rawSemiring n + module RS = RawSemiring vecSemiring + + open VecSemiringProperties rawSemiring n public + open CommutativeMonoidProperties +-commutativeMonoid n public using (+ᴹ-isCommutativeMonoid) + + +ᴹ-*-isSemiringWithoutAnnihilatingZero + : IsSemiringWithoutAnnihilatingZero RS._≈_ RS._+_ RS._*_ RS.0# RS.1# + +ᴹ-*-isSemiringWithoutAnnihilatingZero = record + { +-isCommutativeMonoid = +ᴹ-isCommutativeMonoid + ; *-cong = λ x≈y u≈v i → SWAZ.*-cong (x≈y i) (u≈v i) + ; *-assoc = λ xs ys zs i → SWAZ.*-assoc (xs i) (ys i) (zs i) + ; *-identity = let idˡ , idʳ = SWAZ.*-identity in + (λ xs i → idˡ (xs i)) , (λ xs i → idʳ (xs i)) + ; distrib = let dˡ , dʳ = SWAZ.distrib in + (λ xs ys zs i → dˡ (xs i) (ys i) (zs i)) + , (λ xs ys zs i → dʳ (xs i) (ys i) (zs i)) + } + + +ᴹ-*-semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero _ _ + +ᴹ-*-semiringWithoutAnnihilatingZero = + record { isSemiringWithoutAnnihilatingZero = +ᴹ-*-isSemiringWithoutAnnihilatingZero } + +------------------------------------------------------------------------ + +module SemiringProperties {a ℓ} (semiring : Semiring a ℓ) (n : ℕ) where + module S = Semiring semiring + + private + vecNearSemiring = VecRawNearSemiring S.rawNearSemiring n + vecSemiring = VecRawSemiring S.rawSemiring n + module RNS = RawNearSemiring vecNearSemiring + module RS = RawSemiring vecSemiring + vecLeftSemi = VecRawLeftSemimodule S.rawNearSemiring n + vecRightSemi = VecRawRightSemimodule S.rawNearSemiring n + module LSM = RawLeftSemimodule vecLeftSemi + module RSM = RawRightSemimodule vecRightSemi + + module RN = RawNearSemiringProperties semiring n + + isPreleftSemimodule : IsPreleftSemimodule semiring RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ + isPreleftSemimodule = RN.isPreleftSemimoduleVec + + isPrerightSemimodule : IsPrerightSemimodule semiring RNS._≈_ RNS._+_ RNS.0# RSM._*ᵣ_ + isPrerightSemimodule = RN.isPrerightSemimoduleVec + + isRightSemimodule : IsRightSemimodule semiring RNS._≈_ RNS._+_ RNS.0# RSM._*ᵣ_ + isRightSemimodule = record + { +ᴹ-isCommutativeMonoid = IsBisemimodule.+ᴹ-isCommutativeMonoid RN.isBisemimoduleVec + ; isPrerightSemimodule = isPrerightSemimodule + } + + isBisemimodule : IsBisemimodule semiring semiring RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ RSM._*ᵣ_ + isBisemimodule = RN.isBisemimoduleVec + + isLeftSemimodule : IsLeftSemimodule semiring RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ + isLeftSemimodule = record + { +ᴹ-isCommutativeMonoid = IsBisemimodule.+ᴹ-isCommutativeMonoid RN.isBisemimoduleVec + ; isPreleftSemimodule = isPreleftSemimodule + } + + +ᴹ-*-isSemiring : IsSemiring RS._≈_ RS._+_ RS._*_ RS.0# RS.1# + +ᴹ-*-isSemiring = RN.isSemiringVec + + leftSemimodule : LeftSemimodule _ _ _ + leftSemimodule = record { isLeftSemimodule = isLeftSemimodule } + + +ᴹ-*-semiring : Semiring _ _ + +ᴹ-*-semiring = record { isSemiring = +ᴹ-*-isSemiring } + + +------------------------------------------------------------------------ + +module CommutativeSemiringProperties (commutativeSemiring : CommutativeSemiring a ℓ) (n : ℕ) where + open CommutativeSemiring commutativeSemiring + private + module SR = RawSemiring rawSemiring + baseNearSemiring = SR.rawNearSemiring + + vecSemiring = VecRawSemiring rawSemiring n + vecNearSemiring = VecRawNearSemiring baseNearSemiring n + module RS = RawSemiring vecSemiring + module RNS = RawNearSemiring vecNearSemiring + + module CS = CommutativeSemiring commutativeSemiring + + open SemiringProperties semiring n public + + +ᴹ-*-isCommutativeSemiring : IsCommutativeSemiring RS._≈_ RS._+_ RS._*_ RS.0# RS.1# + +ᴹ-*-isCommutativeSemiring = record + { isSemiring = +ᴹ-*-isSemiring + ; *-comm = λ xs ys i → CS.*-comm (xs i) (ys i) + } + + +ᴹ-*-commutativeSemiring : CommutativeSemiring _ _ + +ᴹ-*-commutativeSemiring = record + { isCommutativeSemiring = +ᴹ-*-isCommutativeSemiring } + +------------------------------------------------------------------------ + +module RingWithoutOneProperties (ringWithoutOne : RingWithoutOne a ℓ) (n : ℕ) where + open RingWithoutOne ringWithoutOne + + private + baseNearSemiring : RawNearSemiring a ℓ + baseNearSemiring = record + { Carrier = Carrier ; _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; 0# = 0# } + + vecNearSemiring = VecRawNearSemiring baseNearSemiring n + module RNS = RawNearSemiring vecNearSemiring + + private + module +G = Group +-group + addRawGroup = +G.rawGroup + vecAddGroup = VecRawGroup addRawGroup n + module VG = RawGroup vecAddGroup + + open AbelianGroupProperties +-abelianGroup n using (+ᴹ-isAbelianGroup) public + + private + module RW1 = IsRingWithoutOne (RingWithoutOne.isRingWithoutOne ringWithoutOne) + + +ᴹ-*-isRingWithoutOne + : IsRingWithoutOne RNS._≈_ RNS._+_ RNS._*_ VG._⁻¹ RNS.0# + +ᴹ-*-isRingWithoutOne = record + { +-isAbelianGroup = +ᴹ-isAbelianGroup + ; *-cong = λ x≈y u≈v i → RW1.*-cong (x≈y i) (u≈v i) + ; *-assoc = λ xs ys zs i → RW1.*-assoc (xs i) (ys i) (zs i) + ; distrib = let dₗ , dᵣ = RW1.distrib in + (λ xs ys zs i → dₗ (xs i) (ys i) (zs i)) + , (λ xs ys zs i → dᵣ (xs i) (ys i) (zs i)) + } + + +ᴹ-*-ringWithoutOne : RingWithoutOne _ _ + +ᴹ-*-ringWithoutOne = record { isRingWithoutOne = +ᴹ-*-isRingWithoutOne } +------------------------------------------------------------------------ + +module RingProperties (ring : Ring a ℓ) (n : ℕ) where + open Ring ring + + private + module S = Semiring semiring + module SR = RawSemiring S.rawSemiring + baseNearSemiring = SR.rawNearSemiring + + vecNearSemiring = VecRawNearSemiring baseNearSemiring n + vecSemiring = VecRawSemiring S.rawSemiring n + module RNS = RawNearSemiring vecNearSemiring + module RS = RawSemiring vecSemiring + + vecLeftSemi = VecRawLeftSemimodule baseNearSemiring n + vecRightSemi = VecRawRightSemimodule baseNearSemiring n + module LSM = RawLeftSemimodule vecLeftSemi + module RSM = RawRightSemimodule vecRightSemi + + module +G = Group +-group + addRawGroup = +G.rawGroup + vecAddGroup = VecRawGroup addRawGroup n + module VG = RawGroup vecAddGroup + + open SemiringProperties semiring n public + open AbelianGroupProperties +-abelianGroup n public + using (+ᴹ-isAbelianGroup; -ᴹ‿cong; -ᴹ‿inverse) + + isRightModule : IsRightModule ring RNS._≈_ RNS._+_ RNS.0# VG._⁻¹ RSM._*ᵣ_ + isRightModule = record + { isRightSemimodule = isRightSemimodule + ; -ᴹ‿cong = -ᴹ‿cong -‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse -‿inverse + } + + isBimodule : IsBimodule ring ring RNS._≈_ RNS._+_ RNS.0# VG._⁻¹ LSM._*ₗ_ RSM._*ᵣ_ + isBimodule = record + { isBisemimodule = isBisemimodule + ; -ᴹ‿cong = -ᴹ‿cong -‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse -‿inverse + } + + isLeftModule : IsLeftModule ring RNS._≈_ RNS._+_ RNS.0# VG._⁻¹ LSM._*ₗ_ + isLeftModule = record + { isLeftSemimodule = isLeftSemimodule + ; -ᴹ‿cong = -ᴹ‿cong -‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse -‿inverse + } + + +ᴹ-*-isRing : IsRing RS._≈_ RS._+_ RS._*_ VG._⁻¹ RS.0# RS.1# + +ᴹ-*-isRing = record + { +-isAbelianGroup = +ᴹ-isAbelianGroup + ; *-cong = λ x≈y u≈v i → *-cong (x≈y i) (u≈v i) + ; *-assoc = λ xs ys zs i → *-assoc (xs i) (ys i) (zs i) + ; *-identity = let idₗ , idᵣ = *-identity in + (λ xs i → idₗ (xs i)) , (λ xs i → idᵣ (xs i)) + ; distrib = let dₗ , dᵣ = distrib in + (λ xs ys zs i → dₗ (xs i) (ys i) (zs i)) + , (λ xs ys zs i → dᵣ (xs i) (ys i) (zs i)) + } + + leftModule : LeftModule _ _ _ + leftModule = record { isLeftModule = isLeftModule } + + bisemimodule : Bisemimodule _ _ _ _ + bisemimodule = record { isBisemimodule = isBisemimodule } + + rightModule : RightModule _ _ _ + rightModule = record { isRightModule = isRightModule } + + bimodule : Bimodule _ _ _ _ + bimodule = record { isBimodule = isBimodule } + +------------------------------------------------------------------------ + +module CommutativeRingProperties (commutativeRing : CommutativeRing a ℓ) (n : ℕ) where + open CommutativeRing commutativeRing + private + module Ri = Ring ring + module S = Semiring Ri.semiring + module SR = RawSemiring S.rawSemiring + baseNearSemiring = SR.rawNearSemiring + + vecNearSemiring = VecRawNearSemiring baseNearSemiring n + vecSemiring = VecRawSemiring S.rawSemiring n + + module RNS = RawNearSemiring vecNearSemiring + module RS = RawSemiring vecSemiring + + vecLeftSemi = VecRawLeftSemimodule baseNearSemiring n + vecRightSemi = VecRawRightSemimodule baseNearSemiring n + module LSM = RawLeftSemimodule vecLeftSemi + module RSM = RawRightSemimodule vecRightSemi + + module +G = Group Ri.+-group + addRawGroup = +G.rawGroup + vecAddGroup = VecRawGroup addRawGroup n + module VG = RawGroup vecAddGroup + + open RingProperties ring n public + + +ᴹ-*-isCommutativeRing + : IsCommutativeRing RS._≈_ RS._+_ RS._*_ VG._⁻¹ RS.0# RS.1# + +ᴹ-*-isCommutativeRing = record + { isRing = +ᴹ-*-isRing + ; *-comm = λ xs ys i → *-comm (xs i) (ys i) + } + + private + *ₗ-*ᵣ-coincident : SimultaneousBiDefs.Coincident Carrier RNS._≈_ LSM._*ₗ_ RSM._*ᵣ_ + *ₗ-*ᵣ-coincident r xs i = *-comm r (xs i) + + isModule : IsModule commutativeRing RNS._≈_ RNS._+_ RNS.0# VG._⁻¹ LSM._*ₗ_ RSM._*ᵣ_ + isModule = record + { isBimodule = isBimodule + ; *ₗ-*ᵣ-coincident = λ r xs i → *-comm r (xs i) + } + + module' : Module _ _ _ + module' = record { isModule = isModule } \ No newline at end of file From c36797b4f5279b6930426bd030457856e7b38c97 Mon Sep 17 00:00:00 2001 From: e-mniang Date: Thu, 28 Aug 2025 19:06:03 -0400 Subject: [PATCH 2/4] changes after review --- CHANGELOG.md | 2 + src/Data/Vec/Functional/Algebra/Base.agda | 131 +++++++++--------- .../Vec/Functional/Algebra/Properties.agda | 105 +++++++------- 3 files changed, 119 insertions(+), 119 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 081dda5b66..aaf9d79e92 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -48,6 +48,8 @@ New modules * `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition. +* `Data.Vec.Functional.Algebra(.{Base|Properties})` - structures and bundles about functional vectors and modules. + Additions to existing modules ----------------------------- diff --git a/src/Data/Vec/Functional/Algebra/Base.agda b/src/Data/Vec/Functional/Algebra/Base.agda index e79c001267..d4345ff3c5 100644 --- a/src/Data/Vec/Functional/Algebra/Base.agda +++ b/src/Data/Vec/Functional/Algebra/Base.agda @@ -24,119 +24,116 @@ private variable A : Set ℓ n : ℕ --- Vector relation lifting -VecRel : {A : Set a} → Rel A ℓ → Rel (Vector A n) ℓ -VecRel _≈_ xs ys = Pointwise _≈_ xs ys +------------------------------------------------------------------------ +-- Vector-lifted relations & operators + +pointwiseᵛ : {A : Set a} ( _≈_ : Rel A ℓ ) → Rel (Vector A n) ℓ +pointwiseᵛ _≈_ = Pointwise _≈_ --- Binary operation lifting -lift₂ᴹ : {A : Set a} → Op₂ A → Op₂ (Vector A n) -lift₂ᴹ _∙_ = zipWith _∙_ +zipWithᵛ : {A : Set a} → Op₂ A → Op₂ (Vector A n) +zipWithᵛ _∙_ = zipWith _∙_ --- Unary operation lifting -lift₁ᴹ : {A : Set a} → Op₁ A → Op₁ (Vector A n) -lift₁ᴹ f = map f +mapᵛ : {A : Set a} → Op₁ A → Op₁ (Vector A n) +mapᵛ f = map f + +------------------------------------------------------------------------ +-- Vector-lifted raw structures --- Vector RawMagma construction -VecRawMagma : RawMagma a ℓ → (n : ℕ) → RawMagma a ℓ -VecRawMagma M n = +rawMagmaᵛ : RawMagma a ℓ → (n : ℕ) → RawMagma a ℓ +rawMagmaᵛ M n = record { Carrier = Vector M.Carrier n - ; _≈_ = VecRel M._≈_ - ; _∙_ = lift₂ᴹ M._∙_ + ; _≈_ = pointwiseᵛ M._≈_ + ; _∙_ = zipWithᵛ M._∙_ } where module M = RawMagma M --- Vector RawMonoid construction -VecRawMonoid : RawMonoid a ℓ → (n : ℕ) → RawMonoid a ℓ -VecRawMonoid M n = +rawMonoidᵛ : RawMonoid a ℓ → (n : ℕ) → RawMonoid a ℓ +rawMonoidᵛ M n = record - { RawMagma (VecRawMagma M.rawMagma n) - ; ε = λ _ → M.ε + { RawMagma (rawMagmaᵛ M.rawMagma n) + ; ε = λ _ → M.ε } - where - module M = RawMonoid M + where module M = RawMonoid M --- Vector RawGroup construction -VecRawGroup : RawGroup a ℓ → (n : ℕ) → RawGroup a ℓ -VecRawGroup G n = +rawGroupᵛ : RawGroup a ℓ → (n : ℕ) → RawGroup a ℓ +rawGroupᵛ G n = record - { RawMonoid (VecRawMonoid G.rawMonoid n) - ; _⁻¹ = lift₁ᴹ G._⁻¹ + { RawMonoid (rawMonoidᵛ G.rawMonoid n) + ; _⁻¹ = mapᵛ G._⁻¹ } where module G = RawGroup G --- Vector RawNearSemiring construction -VecRawNearSemiring : RawNearSemiring a ℓ → (n : ℕ) → RawNearSemiring a ℓ -VecRawNearSemiring NS n = +rawNearSemiringᵛ : RawNearSemiring a ℓ → (n : ℕ) → RawNearSemiring a ℓ +rawNearSemiringᵛ NS n = record { Carrier = Vector NS.Carrier n - ; _≈_ = VecRel NS._≈_ - ; _+_ = lift₂ᴹ NS._+_ - ; _*_ = lift₂ᴹ NS._*_ - ; 0# = λ _ → NS.0# + ; _≈_ = pointwiseᵛ NS._≈_ + ; _+_ = zipWithᵛ NS._+_ + ; _*_ = zipWithᵛ NS._*_ + ; 0# = λ _ → NS.0# } where module NS = RawNearSemiring NS --- Vector RawSemiring construction -VecRawSemiring : RawSemiring a ℓ → (n : ℕ) → RawSemiring a ℓ -VecRawSemiring S n = +rawSemiringᵛ : RawSemiring a ℓ → (n : ℕ) → RawSemiring a ℓ +rawSemiringᵛ S n = record - { RawNearSemiring (VecRawNearSemiring S.rawNearSemiring n) + { RawNearSemiring (rawNearSemiringᵛ S.rawNearSemiring n) ; 1# = λ _ → S.1# } where module S = RawSemiring S --- Vector RawRing construction -VecRawRing : RawRing a ℓ → (n : ℕ) → RawRing a ℓ -VecRawRing R n = +rawRingᵛ : RawRing a ℓ → (n : ℕ) → RawRing a ℓ +rawRingᵛ R n = record - { RawSemiring (VecRawSemiring R.rawSemiring n) - ; -_ = lift₁ᴹ R.-_ + { RawSemiring (rawSemiringᵛ R.rawSemiring n) + ; -_ = mapᵛ R.-_ } where module R = RawRing R +------------------------------------------------------------------------ +-- Vector actions (left/right scalar multiplication) +_*ₗᵛ_ : {S : Set a} → Op₂ S → Opₗ S (Vector S n) +_*ₗᵛ_ _*_ r xs = map (r *_) xs --- Left scalar action obtained from the ring/semiring multiplication -_*ₗ_ : {S : Set a} → Op₂ S → Opₗ S (Vector S n) -_*ₗ_ _*_ r xs = map (λ x → _*_ r x) xs - --- Right scalar action (same underlying Op₂, but as a right action) -_*ᵣ_ : {S : Set a} → Op₂ S → Opᵣ S (Vector S n) -_*ᵣ_ _*_ xs r = map (λ x → _*_ x r) xs +_*ᵣᵛ_ : {S : Set a} → Op₂ S → Opᵣ S (Vector S n) +_*ᵣᵛ_ _*_ xs r = map (_* r) xs +------------------------------------------------------------------------ +-- Vector-lifted semimodule bundles -VecRawLeftSemimodule : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawLeftSemimodule (RawNearSemiring.Carrier NS) a ℓ -VecRawLeftSemimodule NS n = +rawLeftSemimoduleᵛ : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawLeftSemimodule (RawNearSemiring.Carrier NS) a ℓ +rawLeftSemimoduleᵛ NS n = record { Carrierᴹ = Vector NS.Carrier n - ; _≈ᴹ_ = VecRel NS._≈_ - ; _+ᴹ_ = lift₂ᴹ NS._+_ - ; _*ₗ_ = _*ₗ_ NS._*_ + ; _≈ᴹ_ = pointwiseᵛ NS._≈_ + ; _+ᴹ_ = zipWithᵛ NS._+_ + ; _*ₗ_ = _*ₗᵛ_ NS._*_ ; 0ᴹ = λ _ → NS.0# } where module NS = RawNearSemiring NS -VecRawRightSemimodule : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawRightSemimodule (RawNearSemiring.Carrier NS) a ℓ -VecRawRightSemimodule NS n = +rawRightSemimoduleᵛ : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawRightSemimodule (RawNearSemiring.Carrier NS) a ℓ +rawRightSemimoduleᵛ NS n = record { Carrierᴹ = Vector NS.Carrier n - ; _≈ᴹ_ = VecRel NS._≈_ - ; _+ᴹ_ = lift₂ᴹ NS._+_ - ; _*ᵣ_ = _*ᵣ_ NS._*_ + ; _≈ᴹ_ = pointwiseᵛ NS._≈_ + ; _+ᴹ_ = zipWithᵛ NS._+_ + ; _*ᵣ_ = _*ᵣᵛ_ NS._*_ ; 0ᴹ = λ _ → NS.0# } where module NS = RawNearSemiring NS -VecRawBisemimodule : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawBisemimodule (RawNearSemiring.Carrier NS) - (RawNearSemiring.Carrier NS) a ℓ -VecRawBisemimodule NS n = +rawBisemimoduleᵛ : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawBisemimodule (RawNearSemiring.Carrier NS) + (RawNearSemiring.Carrier NS) a ℓ +rawBisemimoduleᵛ NS n = record { Carrierᴹ = Vector NS.Carrier n - ; _≈ᴹ_ = VecRel NS._≈_ - ; _+ᴹ_ = lift₂ᴹ NS._+_ - ; _*ₗ_ = _*ₗ_ NS._*_ - ; _*ᵣ_ = _*ᵣ_ NS._*_ + ; _≈ᴹ_ = pointwiseᵛ NS._≈_ + ; _+ᴹ_ = zipWithᵛ NS._+_ + ; _*ₗ_ = _*ₗᵛ_ NS._*_ + ; _*ᵣ_ = _*ᵣᵛ_ NS._*_ ; 0ᴹ = λ _ → NS.0# } - where module NS = RawNearSemiring NS + where module NS = RawNearSemiring NS \ No newline at end of file diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index b88b95f1f7..f41eb4982e 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -13,6 +13,7 @@ open import Function using (_$_; flip) open import Data.Product hiding (map) open import Data.Nat using (ℕ) open import Data.Fin using (Fin; zero; suc) +open import Function.Base using (_∘′_; _ˢ_; _∘_) open import Data.Vec.Functional open import Algebra.Core open import Algebra.Bundles @@ -34,7 +35,7 @@ private variable module RawMagmaProperties (rawMagma : RawMagma a ℓ) (n : ℕ) where private - vecMagma = VecRawMagma rawMagma n + vecMagma = rawMagmaᵛ rawMagma n module VM = RawMagma vecMagma module M = RawMagma rawMagma @@ -72,7 +73,7 @@ module RawMagmaProperties (rawMagma : RawMagma a ℓ) (n : ℕ) where module RawMonoidProperties (rawMonoid : RawMonoid a ℓ) (n : ℕ) where private - vecMonoid = VecRawMonoid rawMonoid n + vecMonoid = rawMonoidᵛ rawMonoid n module VM = RawMonoid vecMonoid module RM = RawMonoid rawMonoid @@ -107,7 +108,7 @@ module RawMonoidProperties (rawMonoid : RawMonoid a ℓ) (n : ℕ) where module RawGroupProperties (rawGroup : RawGroup a ℓ) (n : ℕ) where private - vecGroup = VecRawGroup rawGroup n + vecGroup = rawGroupᵛ rawGroup n module RG = RawGroup vecGroup module G = RawGroup rawGroup open RawMonoidProperties (RawGroup.rawMonoid rawGroup) n public @@ -149,12 +150,10 @@ module VecSemiringProperties (rawSemiring : RawSemiring a ℓ) (n : ℕ) where module SR = RawSemiring rawSemiring rawNearSemiring = SR.rawNearSemiring module NS = RawNearSemiring rawNearSemiring - vecNearSemiring = VecRawNearSemiring rawNearSemiring n - vecSemiring = VecRawSemiring rawSemiring n + vecNearSemiring = rawNearSemiringᵛ rawNearSemiring n module RNS = RawNearSemiring vecNearSemiring - module RS = RawSemiring vecSemiring - vecLeftSemi = VecRawLeftSemimodule rawNearSemiring n - vecRightSemi = VecRawRightSemimodule rawNearSemiring n + vecLeftSemi = rawLeftSemimoduleᵛ rawNearSemiring n + vecRightSemi = rawRightSemimoduleᵛ rawNearSemiring n module LSM = RawLeftSemimodule vecLeftSemi module RSM = RawRightSemimodule vecRightSemi @@ -178,10 +177,10 @@ module RawNearSemiringProperties {ℓ ℓr} (R : Semiring ℓ ℓr) (n : ℕ) wh open Semiring R private module SR = RawSemiring rawSemiring - vecLeftSemi = VecRawLeftSemimodule rawNearSemiring n - vecRightSemi = VecRawRightSemimodule rawNearSemiring n + vecLeftSemi = rawLeftSemimoduleᵛ rawNearSemiring n + vecRightSemi = rawRightSemimoduleᵛ rawNearSemiring n module LSM = RawLeftSemimodule vecLeftSemi - vecNearSemiring = VecRawNearSemiring rawNearSemiring n + vecNearSemiring = rawNearSemiringᵛ rawNearSemiring n module RNS = RawNearSemiring vecNearSemiring module RSM = RawRightSemimodule vecRightSemi module NS = RawNearSemiring rawNearSemiring @@ -227,23 +226,25 @@ module RawNearSemiringProperties {ℓ ℓr} (R : Semiring ℓ ℓr) (n : ℕ) wh vec1# = λ _ → SR.1# isSemiringVec : IsSemiring RNS._≈_ RNS._+_ RNS._*_ RNS.0# vec1# - isSemiringVec = record { - isSemiringWithoutAnnihilatingZero = record - { +-isCommutativeMonoid = isCommutativeMonoid n +-isCommutativeMonoid - ; *-cong = λ x≈y u≈v i → *-cong (x≈y i) (u≈v i) - ; *-assoc = λ xs ys zs i → *-assoc (xs i) (ys i) (zs i) - ; *-identity = (λ xs i → *-identityˡ (xs i)) , (λ xs i → *-identityʳ (xs i)) - ; distrib = (λ xs ys zs i → distribˡ (xs i) (ys i) (zs i)) , - (λ xs ys zs i → distribʳ (xs i) (ys i) (zs i)) - } - ; zero = (λ xs i → zeroˡ (xs i)) , (λ xs i → zeroʳ (xs i)) } + isSemiringVec = record + { isSemiringWithoutAnnihilatingZero = record + { +-isCommutativeMonoid = isCommutativeMonoid n +-isCommutativeMonoid + ; *-cong = λ x≈y u≈v → ( *-cong ∘ x≈y) ˢ u≈v + ; *-assoc = λ xs ys zs → ((*-assoc ∘ xs) ˢ ys) ˢ zs + ; *-identity = (λ xs → *-identityˡ ∘ xs) + , (λ xs → *-identityʳ ∘ xs) + ; distrib = (λ xs ys zs → ((distribˡ ∘ xs) ˢ ys) ˢ zs) + , (λ xs ys zs → ((distribʳ ∘ xs) ˢ ys) ˢ zs) + } + ; zero = (λ xs → zeroˡ ∘ xs) , (λ xs → zeroʳ ∘ xs) + } ------------------------------------------------------------------------ module MagmaProperties (magma : Magma a ℓ) (n : ℕ) where open Magma magma using (_≈_; _∙_; isMagma; rawMagma) private - vecMagma = VecRawMagma rawMagma n + vecMagma = rawMagmaᵛ rawMagma n module VM = RawMagma vecMagma module RM = RawMagma rawMagma @@ -265,7 +266,7 @@ module MagmaProperties (magma : Magma a ℓ) (n : ℕ) where module CommutativeMagmaProperties (commutativeMagma : CommutativeMagma a ℓ) (n : ℕ) where open CommutativeMagma commutativeMagma private - vecMagma = VecRawMagma rawMagma n + vecMagma = rawMagmaᵛ rawMagma n module VM = RawMagma vecMagma module M = RawMagma rawMagma @@ -283,7 +284,7 @@ module SemiRawGroupProperties (semigroup : Semigroup a ℓ) (n : ℕ) where open Semigroup semigroup private - vecMagma = VecRawMagma rawMagma n + vecMagma = rawMagmaᵛ rawMagma n module VM = RawMagma vecMagma module M = RawMagma rawMagma @@ -301,7 +302,7 @@ module CommutativeSemigroupProperties (commutativeSemigroup : CommutativeSemigro open CommutativeSemigroup commutativeSemigroup private - vecMagma = VecRawMagma rawMagma n + vecMagma = rawMagmaᵛ rawMagma n module VM = RawMagma vecMagma module M = RawMagma rawMagma @@ -318,7 +319,7 @@ module CommutativeSemigroupProperties (commutativeSemigroup : CommutativeSemigro module MonoidProperties (monoid : Monoid a ℓ) (n : ℕ) where open Monoid monoid private - vecMonoid = VecRawMonoid rawMonoid n + vecMonoid = rawMonoidᵛ rawMonoid n module VM = RawMonoid vecMonoid module M = RawMonoid rawMonoid @@ -337,7 +338,7 @@ module CommutativeMonoidProperties (commutativeMonoid : CommutativeMonoid a ℓ) open CommutativeMonoid commutativeMonoid private - vecMonoid = VecRawMonoid rawMonoid n + vecMonoid = rawMonoidᵛ rawMonoid n module VM = RawMonoid vecMonoid module M = RawMonoid rawMonoid @@ -357,7 +358,7 @@ module GroupProperties (group : Group a ℓ) (n : ℕ) where open Group group private - vecGroup = VecRawGroup rawGroup n + vecGroup = rawGroupᵛ rawGroup n module VG = RawGroup vecGroup module G = RawGroup rawGroup @@ -379,7 +380,7 @@ module GroupProperties (group : Group a ℓ) (n : ℕ) where module AbelianGroupProperties (abelianGroup : AbelianGroup a ℓ) (n : ℕ) where open AbelianGroup abelianGroup private - vecGroup = VecRawGroup rawGroup n + vecGroup = rawGroupᵛ rawGroup n module VG = RawGroup vecGroup open GroupProperties group n public @@ -399,7 +400,7 @@ module NearSemiringProperties (nearSemiring : NearSemiring a ℓ) (n : ℕ) wher open NearSemiring nearSemiring private module N = NearSemiring nearSemiring - vecNearSemiring = VecRawNearSemiring rawNearSemiring n + vecNearSemiring = rawNearSemiringᵛ rawNearSemiring n module RNS = RawNearSemiring vecNearSemiring open MonoidProperties +-monoid n public using (+ᴹ-isMonoid) @@ -422,7 +423,7 @@ module NearSemiringProperties (nearSemiring : NearSemiring a ℓ) (n : ℕ) wher module SemiringWithoutOneProperties (semiringWithoutOne : SemiringWithoutOne a ℓ) (n : ℕ) where open SemiringWithoutOne semiringWithoutOne private - vecNearSemiring = VecRawNearSemiring rawNearSemiring n + vecNearSemiring = rawNearSemiringᵛ rawNearSemiring n module RNS = RawNearSemiring vecNearSemiring module SWO = SemiringWithoutOne semiringWithoutOne @@ -450,7 +451,7 @@ module CommutativeSemiringWithoutOneProperties open CommutativeSemiringWithoutOne commutativeSemiringWithoutOne private module CSWO = CommutativeSemiringWithoutOne commutativeSemiringWithoutOne - vecNearSemiring = VecRawNearSemiring rawNearSemiring n + vecNearSemiring = rawNearSemiringᵛ rawNearSemiring n module RNS = RawNearSemiring vecNearSemiring open SemiringWithoutOneProperties semiringWithoutOne n public @@ -476,7 +477,7 @@ module SemiringWithoutAnnihilatingZeroProperties private module SWAZ = SemiringWithoutAnnihilatingZero semiringWithoutAnnihilatingZero - vecSemiring = VecRawSemiring rawSemiring n + vecSemiring = rawSemiringᵛ rawSemiring n module RS = RawSemiring vecSemiring open VecSemiringProperties rawSemiring n public @@ -505,12 +506,12 @@ module SemiringProperties {a ℓ} (semiring : Semiring a ℓ) (n : ℕ) where module S = Semiring semiring private - vecNearSemiring = VecRawNearSemiring S.rawNearSemiring n - vecSemiring = VecRawSemiring S.rawSemiring n + vecNearSemiring = rawNearSemiringᵛ S.rawNearSemiring n + vecSemiring = rawSemiringᵛ S.rawSemiring n module RNS = RawNearSemiring vecNearSemiring module RS = RawSemiring vecSemiring - vecLeftSemi = VecRawLeftSemimodule S.rawNearSemiring n - vecRightSemi = VecRawRightSemimodule S.rawNearSemiring n + vecLeftSemi = rawLeftSemimoduleᵛ S.rawNearSemiring n + vecRightSemi = rawRightSemimoduleᵛ S.rawNearSemiring n module LSM = RawLeftSemimodule vecLeftSemi module RSM = RawRightSemimodule vecRightSemi @@ -546,7 +547,6 @@ module SemiringProperties {a ℓ} (semiring : Semiring a ℓ) (n : ℕ) where +ᴹ-*-semiring : Semiring _ _ +ᴹ-*-semiring = record { isSemiring = +ᴹ-*-isSemiring } - ------------------------------------------------------------------------ module CommutativeSemiringProperties (commutativeSemiring : CommutativeSemiring a ℓ) (n : ℕ) where @@ -555,8 +555,8 @@ module CommutativeSemiringProperties (commutativeSemiring : CommutativeSemiring module SR = RawSemiring rawSemiring baseNearSemiring = SR.rawNearSemiring - vecSemiring = VecRawSemiring rawSemiring n - vecNearSemiring = VecRawNearSemiring baseNearSemiring n + vecSemiring = rawSemiringᵛ rawSemiring n + vecNearSemiring = rawNearSemiringᵛ baseNearSemiring n module RS = RawSemiring vecSemiring module RNS = RawNearSemiring vecNearSemiring @@ -584,13 +584,13 @@ module RingWithoutOneProperties (ringWithoutOne : RingWithoutOne a ℓ) (n : ℕ baseNearSemiring = record { Carrier = Carrier ; _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; 0# = 0# } - vecNearSemiring = VecRawNearSemiring baseNearSemiring n + vecNearSemiring = rawNearSemiringᵛ baseNearSemiring n module RNS = RawNearSemiring vecNearSemiring private module +G = Group +-group addRawGroup = +G.rawGroup - vecAddGroup = VecRawGroup addRawGroup n + vecAddGroup = rawGroupᵛ addRawGroup n module VG = RawGroup vecAddGroup open AbelianGroupProperties +-abelianGroup n using (+ᴹ-isAbelianGroup) public @@ -611,6 +611,7 @@ module RingWithoutOneProperties (ringWithoutOne : RingWithoutOne a ℓ) (n : ℕ +ᴹ-*-ringWithoutOne : RingWithoutOne _ _ +ᴹ-*-ringWithoutOne = record { isRingWithoutOne = +ᴹ-*-isRingWithoutOne } + ------------------------------------------------------------------------ module RingProperties (ring : Ring a ℓ) (n : ℕ) where @@ -621,19 +622,19 @@ module RingProperties (ring : Ring a ℓ) (n : ℕ) where module SR = RawSemiring S.rawSemiring baseNearSemiring = SR.rawNearSemiring - vecNearSemiring = VecRawNearSemiring baseNearSemiring n - vecSemiring = VecRawSemiring S.rawSemiring n + vecNearSemiring = rawNearSemiringᵛ baseNearSemiring n + vecSemiring = rawSemiringᵛ S.rawSemiring n module RNS = RawNearSemiring vecNearSemiring module RS = RawSemiring vecSemiring - vecLeftSemi = VecRawLeftSemimodule baseNearSemiring n - vecRightSemi = VecRawRightSemimodule baseNearSemiring n + vecLeftSemi = rawLeftSemimoduleᵛ baseNearSemiring n + vecRightSemi = rawRightSemimoduleᵛ baseNearSemiring n module LSM = RawLeftSemimodule vecLeftSemi module RSM = RawRightSemimodule vecRightSemi module +G = Group +-group addRawGroup = +G.rawGroup - vecAddGroup = VecRawGroup addRawGroup n + vecAddGroup = rawGroupᵛ addRawGroup n module VG = RawGroup vecAddGroup open SemiringProperties semiring n public @@ -695,20 +696,20 @@ module CommutativeRingProperties (commutativeRing : CommutativeRing a ℓ) (n : module SR = RawSemiring S.rawSemiring baseNearSemiring = SR.rawNearSemiring - vecNearSemiring = VecRawNearSemiring baseNearSemiring n - vecSemiring = VecRawSemiring S.rawSemiring n + vecNearSemiring = rawNearSemiringᵛ baseNearSemiring n + vecSemiring = rawSemiringᵛ S.rawSemiring n module RNS = RawNearSemiring vecNearSemiring module RS = RawSemiring vecSemiring - vecLeftSemi = VecRawLeftSemimodule baseNearSemiring n - vecRightSemi = VecRawRightSemimodule baseNearSemiring n + vecLeftSemi = rawLeftSemimoduleᵛ baseNearSemiring n + vecRightSemi = rawRightSemimoduleᵛ baseNearSemiring n module LSM = RawLeftSemimodule vecLeftSemi module RSM = RawRightSemimodule vecRightSemi module +G = Group Ri.+-group addRawGroup = +G.rawGroup - vecAddGroup = VecRawGroup addRawGroup n + vecAddGroup = rawGroupᵛ addRawGroup n module VG = RawGroup vecAddGroup open RingProperties ring n public From e67c13e94694a1989a4f3c3ab57e42746f21ebf7 Mon Sep 17 00:00:00 2001 From: e-mniang Date: Fri, 29 Aug 2025 19:51:02 -0400 Subject: [PATCH 3/4] names changes --- src/Data/Vec/Functional/Algebra/Base.agda | 8 +- .../Vec/Functional/Algebra/Properties.agda | 282 +++++++++--------- 2 files changed, 140 insertions(+), 150 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Base.agda b/src/Data/Vec/Functional/Algebra/Base.agda index d4345ff3c5..61d66b4d9d 100644 --- a/src/Data/Vec/Functional/Algebra/Base.agda +++ b/src/Data/Vec/Functional/Algebra/Base.agda @@ -21,19 +21,19 @@ open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise) private variable a ℓ : Level - A : Set ℓ + A : Set a n : ℕ ------------------------------------------------------------------------ -- Vector-lifted relations & operators -pointwiseᵛ : {A : Set a} ( _≈_ : Rel A ℓ ) → Rel (Vector A n) ℓ +pointwiseᵛ : ( _≈_ : Rel A ℓ ) → Rel (Vector A n) ℓ pointwiseᵛ _≈_ = Pointwise _≈_ -zipWithᵛ : {A : Set a} → Op₂ A → Op₂ (Vector A n) +zipWithᵛ : Op₂ A → Op₂ (Vector A n) zipWithᵛ _∙_ = zipWith _∙_ -mapᵛ : {A : Set a} → Op₁ A → Op₁ (Vector A n) +mapᵛ : Op₁ A → Op₁ (Vector A n) mapᵛ f = map f ------------------------------------------------------------------------ diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index f41eb4982e..deca24132a 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -20,7 +20,7 @@ open import Algebra.Bundles open import Algebra.Module open import Algebra.Module.Structures open import Relation.Binary -import Algebra.Definitions as ADefinitions +import Algebra.Definitions as Definitions open import Algebra.Structures open import Data.Vec.Functional.Algebra.Base import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as Pointwise @@ -35,36 +35,36 @@ private variable module RawMagmaProperties (rawMagma : RawMagma a ℓ) (n : ℕ) where private - vecMagma = rawMagmaᵛ rawMagma n - module VM = RawMagma vecMagma + magmaᵛ = rawMagmaᵛ rawMagma n + module VM = RawMagma magmaᵛ module M = RawMagma rawMagma open IsEquivalence - isMagma : IsMagma M._≈_ M._∙_ → IsMagma VM._≈_ VM._∙_ - isMagma base = record + isMagmaᵛ : IsMagma M._≈_ M._∙_ → IsMagma VM._≈_ VM._∙_ + isMagmaᵛ base = record { isEquivalence = flip Pointwise.isEquivalence _ B.isEquivalence ; ∙-cong = λ x≈y u≈v i → B.∙-cong (x≈y i) (u≈v i) } where module B = IsMagma base - isCommutativeMagma : IsCommutativeMagma M._≈_ M._∙_ → IsCommutativeMagma VM._≈_ VM._∙_ - isCommutativeMagma base = record - { isMagma = isMagma CM.isMagma + isCommutativeMagmaᵛ : IsCommutativeMagma M._≈_ M._∙_ → IsCommutativeMagma VM._≈_ VM._∙_ + isCommutativeMagmaᵛ base = record + { isMagma = isMagmaᵛ CM.isMagma ; comm = λ xs ys i → CM.comm (xs i) (ys i) } where module CM = IsCommutativeMagma base - isSemigroup : IsSemigroup M._≈_ M._∙_ → IsSemigroup VM._≈_ VM._∙_ - isSemigroup base = record - { isMagma = isMagma SG.isMagma + isSemigroupᵛ : IsSemigroup M._≈_ M._∙_ → IsSemigroup VM._≈_ VM._∙_ + isSemigroupᵛ base = record + { isMagma = isMagmaᵛ SG.isMagma ; assoc = λ xs ys zs i → SG.assoc (xs i) (ys i) (zs i) } where module SG = IsSemigroup base - isCommutativeSemigroup : IsCommutativeSemigroup M._≈_ M._∙_ → IsCommutativeSemigroup VM._≈_ VM._∙_ - isCommutativeSemigroup base = record - { isSemigroup = isSemigroup CS.isSemigroup + isCommutativeSemigroupᵛ : IsCommutativeSemigroup M._≈_ M._∙_ → IsCommutativeSemigroup VM._≈_ VM._∙_ + isCommutativeSemigroupᵛ base = record + { isSemigroup = isSemigroupᵛ CS.isSemigroup ; comm = λ xs ys i → CS.comm (xs i) (ys i) } where module CS = IsCommutativeSemigroup base @@ -73,15 +73,15 @@ module RawMagmaProperties (rawMagma : RawMagma a ℓ) (n : ℕ) where module RawMonoidProperties (rawMonoid : RawMonoid a ℓ) (n : ℕ) where private - vecMonoid = rawMonoidᵛ rawMonoid n - module VM = RawMonoid vecMonoid + monoidᵛ = rawMonoidᵛ rawMonoid n + module VM = RawMonoid monoidᵛ module RM = RawMonoid rawMonoid open RawMagmaProperties (RawMonoid.rawMagma rawMonoid) n public private - module ≈ = ADefinitions RM._≈_ - module ≈ᴹ = ADefinitions VM._≈_ + module ≈ = Definitions RM._≈_ + module ≈ᴹ = Definitions VM._≈_ +ᴹ-identityˡ : ≈.LeftIdentity RM.ε RM._∙_ → ≈ᴹ.LeftIdentity VM.ε VM._∙_ +ᴹ-identityˡ idˡ xs i = idˡ (xs i) @@ -92,15 +92,15 @@ module RawMonoidProperties (rawMonoid : RawMonoid a ℓ) (n : ℕ) where +ᴹ-identity : ≈.Identity RM.ε RM._∙_ → ≈ᴹ.Identity VM.ε VM._∙_ +ᴹ-identity (idˡ , idʳ) = +ᴹ-identityˡ idˡ , +ᴹ-identityʳ idʳ - isMonoid : IsMonoid RM._≈_ RM._∙_ RM.ε → IsMonoid VM._≈_ VM._∙_ VM.ε - isMonoid isMonoid = record - { isSemigroup = isSemigroup M.isSemigroup + isMonoidᵛ : IsMonoid RM._≈_ RM._∙_ RM.ε → IsMonoid VM._≈_ VM._∙_ VM.ε + isMonoidᵛ isMonoid = record + { isSemigroup = isSemigroupᵛ M.isSemigroup ; identity = +ᴹ-identity M.identity } where module M = IsMonoid isMonoid - isCommutativeMonoid : IsCommutativeMonoid RM._≈_ RM._∙_ RM.ε → IsCommutativeMonoid VM._≈_ VM._∙_ VM.ε - isCommutativeMonoid base = record - { isMonoid = isMonoid CM.isMonoid + isCommutativeMonoidᵛ : IsCommutativeMonoid RM._≈_ RM._∙_ RM.ε → IsCommutativeMonoid VM._≈_ VM._∙_ VM.ε + isCommutativeMonoidᵛ base = record + { isMonoid = isMonoidᵛ CM.isMonoid ; comm = λ xs ys i → CM.comm (xs i) (ys i) } where module CM = IsCommutativeMonoid base @@ -108,14 +108,14 @@ module RawMonoidProperties (rawMonoid : RawMonoid a ℓ) (n : ℕ) where module RawGroupProperties (rawGroup : RawGroup a ℓ) (n : ℕ) where private - vecGroup = rawGroupᵛ rawGroup n - module RG = RawGroup vecGroup + groupᵛ = rawGroupᵛ rawGroup n + module RG = RawGroup groupᵛ module G = RawGroup rawGroup open RawMonoidProperties (RawGroup.rawMonoid rawGroup) n public private - module ≈ = ADefinitions G._≈_ - module ≈ᴹ = ADefinitions RG._≈_ + module ≈ = Definitions G._≈_ + module ≈ᴹ = Definitions RG._≈_ -ᴹ‿inverseˡ : ≈.LeftInverse G.ε G._⁻¹ G._∙_ → ≈ᴹ.LeftInverse RG.ε RG._⁻¹ RG._∙_ -ᴹ‿inverseˡ -‿inverseˡ xs i = -‿inverseˡ (xs i) @@ -129,16 +129,16 @@ module RawGroupProperties (rawGroup : RawGroup a ℓ) (n : ℕ) where -ᴹ‿cong : ≈.Congruent₁ G._⁻¹ → ≈ᴹ.Congruent₁ RG._⁻¹ -ᴹ‿cong -‿cong xs≈ys i = -‿cong (xs≈ys i) - isGroup : IsGroup G._≈_ G._∙_ G.ε G._⁻¹ → IsGroup RG._≈_ RG._∙_ RG.ε RG._⁻¹ - isGroup isGroup = record - { isMonoid = isMonoid M.isMonoid + isGroupᵛ : IsGroup G._≈_ G._∙_ G.ε G._⁻¹ → IsGroup RG._≈_ RG._∙_ RG.ε RG._⁻¹ + isGroupᵛ isGroup = record + { isMonoid = isMonoidᵛ M.isMonoid ; inverse = -ᴹ‿inverse M.inverse ; ⁻¹-cong = -ᴹ‿cong M.⁻¹-cong } where module M = IsGroup isGroup - isAbelianGroup : IsAbelianGroup G._≈_ G._∙_ G.ε G._⁻¹ → IsAbelianGroup RG._≈_ RG._∙_ RG.ε RG._⁻¹ - isAbelianGroup base = record - { isGroup = isGroup AG.isGroup + isAbelianGroupᵛ : IsAbelianGroup G._≈_ G._∙_ G.ε G._⁻¹ → IsAbelianGroup RG._≈_ RG._∙_ RG.ε RG._⁻¹ + isAbelianGroupᵛ base = record + { isGroup = isGroupᵛ AG.isGroup ; comm = λ xs ys i → AG.comm (xs i) (ys i) } where module AG = IsAbelianGroup base @@ -150,19 +150,19 @@ module VecSemiringProperties (rawSemiring : RawSemiring a ℓ) (n : ℕ) where module SR = RawSemiring rawSemiring rawNearSemiring = SR.rawNearSemiring module NS = RawNearSemiring rawNearSemiring - vecNearSemiring = rawNearSemiringᵛ rawNearSemiring n - module RNS = RawNearSemiring vecNearSemiring - vecLeftSemi = rawLeftSemimoduleᵛ rawNearSemiring n - vecRightSemi = rawRightSemimoduleᵛ rawNearSemiring n - module LSM = RawLeftSemimodule vecLeftSemi - module RSM = RawRightSemimodule vecRightSemi + nearSemiringᵛ = rawNearSemiringᵛ rawNearSemiring n + module RNS = RawNearSemiring nearSemiringᵛ + leftSemiᵛ = rawLeftSemimoduleᵛ rawNearSemiring n + rightSemiᵛ = rawRightSemimoduleᵛ rawNearSemiring n + module LSM = RawLeftSemimodule leftSemiᵛ + module RSM = RawRightSemimodule rightSemiᵛ open RawMonoidProperties (RawSemiring.*-rawMonoid rawSemiring) n public using () renaming (+ᴹ-identity to *ᴹ-identity) private - module ≈ = ADefinitions NS._≈_ + module ≈ = Definitions NS._≈_ module LD = LeftDefs NS.Carrier RNS._≈_ module RD = RightDefs NS.Carrier RNS._≈_ @@ -171,24 +171,25 @@ module VecSemiringProperties (rawSemiring : RawSemiring a ℓ) (n : ℕ) where *ᵣ-identityʳ : ≈.RightIdentity SR.1# NS._*_ → RD.RightIdentity SR.1# (λ xs r → RSM._*ᵣ_ xs r) *ᵣ-identityʳ *-idʳ xs i = *-idʳ (xs i) + ------------------------------------------------------------------------ module RawNearSemiringProperties {ℓ ℓr} (R : Semiring ℓ ℓr) (n : ℕ) where open Semiring R private module SR = RawSemiring rawSemiring - vecLeftSemi = rawLeftSemimoduleᵛ rawNearSemiring n - vecRightSemi = rawRightSemimoduleᵛ rawNearSemiring n - module LSM = RawLeftSemimodule vecLeftSemi - vecNearSemiring = rawNearSemiringᵛ rawNearSemiring n - module RNS = RawNearSemiring vecNearSemiring - module RSM = RawRightSemimodule vecRightSemi + leftSemiᵛ = rawLeftSemimoduleᵛ rawNearSemiring n + rightSemiᵛ = rawRightSemimoduleᵛ rawNearSemiring n + module LSM = RawLeftSemimodule leftSemiᵛ + nearSemiringᵛ = rawNearSemiringᵛ rawNearSemiring n + module RNS = RawNearSemiring nearSemiringᵛ + module RSM = RawRightSemimodule rightSemiᵛ module NS = RawNearSemiring rawNearSemiring open RawMonoidProperties +-rawMonoid - isPreleftSemimoduleVec : IsPreleftSemimodule R RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ - isPreleftSemimoduleVec = record + isPreleftSemimoduleᵛ : IsPreleftSemimodule R RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ + isPreleftSemimoduleᵛ = record { *ₗ-cong = λ x≈y u≈v i → *-cong x≈y (u≈v i) ; *ₗ-zeroˡ = λ xs i → zeroˡ (xs i) ; *ₗ-distribʳ = λ xs m n i → distribʳ (xs i) m n @@ -199,8 +200,8 @@ module RawNearSemiringProperties {ℓ ℓr} (R : Semiring ℓ ℓr) (n : ℕ) wh } - isPrerightSemimoduleVec : IsPrerightSemimodule R RNS._≈_ RNS._+_ RNS.0# RSM._*ᵣ_ - isPrerightSemimoduleVec = record + isPrerightSemimoduleᵛ : IsPrerightSemimodule R RNS._≈_ RNS._+_ RNS.0# RSM._*ᵣ_ + isPrerightSemimoduleᵛ = record { *ᵣ-cong = λ x≈y u≈v i → *-cong (x≈y i) u≈v ; *ᵣ-zeroʳ = λ xs i → zeroʳ (xs i) ; *ᵣ-distribˡ = λ xs m n i → distribˡ (xs i) m n @@ -210,25 +211,25 @@ module RawNearSemiringProperties {ℓ ℓr} (R : Semiring ℓ ℓr) (n : ℕ) wh ; *ᵣ-distribʳ = λ xs m n i → distribʳ xs (m i) (n i) } - isBisemimoduleVec : IsBisemimodule R R RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ RSM._*ᵣ_ - isBisemimoduleVec = record - { +ᴹ-isCommutativeMonoid = isCommutativeMonoid n +-isCommutativeMonoid - ; isPreleftSemimodule = isPreleftSemimoduleVec - ; isPrerightSemimodule = isPrerightSemimoduleVec + isBisemimoduleᵛ : IsBisemimodule R R RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ RSM._*ᵣ_ + isBisemimoduleᵛ = record + { +ᴹ-isCommutativeMonoid = isCommutativeMonoidᵛ n +-isCommutativeMonoid + ; isPreleftSemimodule = isPreleftSemimoduleᵛ + ; isPrerightSemimodule = isPrerightSemimoduleᵛ ; *ₗ-*ᵣ-assoc = λ xs m ys i → *-assoc xs (m i) ys } private - module ≈ = ADefinitions NS._≈_ - module ≈ᴹ = ADefinitions RNS._≈_ + module ≈ = Definitions NS._≈_ + module ≈ᴹ = Definitions RNS._≈_ - vec1# : Vector NS.Carrier n - vec1# = λ _ → SR.1# + 1#ᵛ : Vector NS.Carrier n + 1#ᵛ = λ _ → SR.1# - isSemiringVec : IsSemiring RNS._≈_ RNS._+_ RNS._*_ RNS.0# vec1# - isSemiringVec = record + isSemiringᵛ : IsSemiring RNS._≈_ RNS._+_ RNS._*_ RNS.0# 1#ᵛ + isSemiringᵛ = record { isSemiringWithoutAnnihilatingZero = record - { +-isCommutativeMonoid = isCommutativeMonoid n +-isCommutativeMonoid + { +-isCommutativeMonoid = isCommutativeMonoidᵛ n +-isCommutativeMonoid ; *-cong = λ x≈y u≈v → ( *-cong ∘ x≈y) ˢ u≈v ; *-assoc = λ xs ys zs → ((*-assoc ∘ xs) ˢ ys) ˢ zs ; *-identity = (λ xs → *-identityˡ ∘ xs) @@ -244,19 +245,14 @@ module RawNearSemiringProperties {ℓ ℓr} (R : Semiring ℓ ℓr) (n : ℕ) wh module MagmaProperties (magma : Magma a ℓ) (n : ℕ) where open Magma magma using (_≈_; _∙_; isMagma; rawMagma) private - vecMagma = rawMagmaᵛ rawMagma n - module VM = RawMagma vecMagma + magmaᵛ = rawMagmaᵛ rawMagma n + module VM = RawMagma magmaᵛ module RM = RawMagma rawMagma - open RawMagmaProperties rawMagma n public renaming - ( isMagma to vec-isMagma - ; isCommutativeMagma to vec-isCommutativeMagma - ; isSemigroup to vec-isSemigroup - ; isCommutativeSemigroup to vec-isCommutativeSemigroup - ) + open RawMagmaProperties rawMagma n public +ᴹ-isMagma : IsMagma VM._≈_ VM._∙_ - +ᴹ-isMagma = vec-isMagma isMagma + +ᴹ-isMagma = isMagmaᵛ isMagma +ᴹ-magma : Magma _ _ +ᴹ-magma = record { isMagma = +ᴹ-isMagma } @@ -266,14 +262,14 @@ module MagmaProperties (magma : Magma a ℓ) (n : ℕ) where module CommutativeMagmaProperties (commutativeMagma : CommutativeMagma a ℓ) (n : ℕ) where open CommutativeMagma commutativeMagma private - vecMagma = rawMagmaᵛ rawMagma n - module VM = RawMagma vecMagma + magmaᵛ = rawMagmaᵛ rawMagma n + module VM = RawMagma magmaᵛ module M = RawMagma rawMagma open MagmaProperties magma n public +ᴹ-isCommutativeMagma : IsCommutativeMagma VM._≈_ VM._∙_ - +ᴹ-isCommutativeMagma = vec-isCommutativeMagma isCommutativeMagma + +ᴹ-isCommutativeMagma = isCommutativeMagmaᵛ isCommutativeMagma +ᴹ-commutativeMagma : CommutativeMagma _ _ +ᴹ-commutativeMagma = record { isCommutativeMagma = +ᴹ-isCommutativeMagma } @@ -284,14 +280,14 @@ module SemiRawGroupProperties (semigroup : Semigroup a ℓ) (n : ℕ) where open Semigroup semigroup private - vecMagma = rawMagmaᵛ rawMagma n - module VM = RawMagma vecMagma + magmaᵛ = rawMagmaᵛ rawMagma n + module VM = RawMagma magmaᵛ module M = RawMagma rawMagma open MagmaProperties magma n public +ᴹ-isSemigroup : IsSemigroup VM._≈_ VM._∙_ - +ᴹ-isSemigroup = vec-isSemigroup isSemigroup + +ᴹ-isSemigroup = isSemigroupᵛ isSemigroup +ᴹ-semigroup : Semigroup _ _ +ᴹ-semigroup = record { isSemigroup = +ᴹ-isSemigroup } @@ -302,14 +298,14 @@ module CommutativeSemigroupProperties (commutativeSemigroup : CommutativeSemigro open CommutativeSemigroup commutativeSemigroup private - vecMagma = rawMagmaᵛ rawMagma n - module VM = RawMagma vecMagma + magmaᵛ = rawMagmaᵛ rawMagma n + module VM = RawMagma magmaᵛ module M = RawMagma rawMagma open MagmaProperties magma n public +ᴹ-isCommutativeSemigroup : IsCommutativeSemigroup VM._≈_ VM._∙_ - +ᴹ-isCommutativeSemigroup = vec-isCommutativeSemigroup isCommutativeSemigroup + +ᴹ-isCommutativeSemigroup = isCommutativeSemigroupᵛ isCommutativeSemigroup +ᴹ-commutativeSemigroup : CommutativeSemigroup _ _ +ᴹ-commutativeSemigroup = record { isCommutativeSemigroup = +ᴹ-isCommutativeSemigroup } @@ -319,8 +315,8 @@ module CommutativeSemigroupProperties (commutativeSemigroup : CommutativeSemigro module MonoidProperties (monoid : Monoid a ℓ) (n : ℕ) where open Monoid monoid private - vecMonoid = rawMonoidᵛ rawMonoid n - module VM = RawMonoid vecMonoid + monoidᵛ = rawMonoidᵛ rawMonoid n + module VM = RawMonoid monoidᵛ module M = RawMonoid rawMonoid open RawMonoidProperties rawMonoid n public using (+ᴹ-identity) @@ -338,16 +334,14 @@ module CommutativeMonoidProperties (commutativeMonoid : CommutativeMonoid a ℓ) open CommutativeMonoid commutativeMonoid private - vecMonoid = rawMonoidᵛ rawMonoid n - module VM = RawMonoid vecMonoid + monoidᵛ = rawMonoidᵛ rawMonoid n + module VM = RawMonoid monoidᵛ module M = RawMonoid rawMonoid open RawMonoidProperties rawMonoid n - using () - renaming ( isCommutativeMonoid to vec-isCommutativeMonoid ) +ᴹ-isCommutativeMonoid : IsCommutativeMonoid VM._≈_ VM._∙_ VM.ε - +ᴹ-isCommutativeMonoid = vec-isCommutativeMonoid isCommutativeMonoid + +ᴹ-isCommutativeMonoid = isCommutativeMonoidᵛ isCommutativeMonoid +ᴹ-commutativeMonoid : CommutativeMonoid _ _ +ᴹ-commutativeMonoid = record { isCommutativeMonoid = +ᴹ-isCommutativeMonoid } @@ -358,8 +352,8 @@ module GroupProperties (group : Group a ℓ) (n : ℕ) where open Group group private - vecGroup = rawGroupᵛ rawGroup n - module VG = RawGroup vecGroup + groupᵛ = rawGroupᵛ rawGroup n + module VG = RawGroup groupᵛ module G = RawGroup rawGroup open RawGroupProperties rawGroup n public using (-ᴹ‿inverse; -ᴹ‿cong) @@ -380,8 +374,8 @@ module GroupProperties (group : Group a ℓ) (n : ℕ) where module AbelianGroupProperties (abelianGroup : AbelianGroup a ℓ) (n : ℕ) where open AbelianGroup abelianGroup private - vecGroup = rawGroupᵛ rawGroup n - module VG = RawGroup vecGroup + groupᵛ = rawGroupᵛ rawGroup n + module VG = RawGroup groupᵛ open GroupProperties group n public @@ -400,8 +394,8 @@ module NearSemiringProperties (nearSemiring : NearSemiring a ℓ) (n : ℕ) wher open NearSemiring nearSemiring private module N = NearSemiring nearSemiring - vecNearSemiring = rawNearSemiringᵛ rawNearSemiring n - module RNS = RawNearSemiring vecNearSemiring + nearSemiringᵛ = rawNearSemiringᵛ rawNearSemiring n + module RNS = RawNearSemiring nearSemiringᵛ open MonoidProperties +-monoid n public using (+ᴹ-isMonoid) @@ -423,8 +417,8 @@ module NearSemiringProperties (nearSemiring : NearSemiring a ℓ) (n : ℕ) wher module SemiringWithoutOneProperties (semiringWithoutOne : SemiringWithoutOne a ℓ) (n : ℕ) where open SemiringWithoutOne semiringWithoutOne private - vecNearSemiring = rawNearSemiringᵛ rawNearSemiring n - module RNS = RawNearSemiring vecNearSemiring + nearSemiringᵛ = rawNearSemiringᵛ rawNearSemiring n + module RNS = RawNearSemiring nearSemiringᵛ module SWO = SemiringWithoutOne semiringWithoutOne open CommutativeMonoidProperties +-commutativeMonoid n public using (+ᴹ-isCommutativeMonoid) @@ -451,8 +445,8 @@ module CommutativeSemiringWithoutOneProperties open CommutativeSemiringWithoutOne commutativeSemiringWithoutOne private module CSWO = CommutativeSemiringWithoutOne commutativeSemiringWithoutOne - vecNearSemiring = rawNearSemiringᵛ rawNearSemiring n - module RNS = RawNearSemiring vecNearSemiring + nearSemiringᵛ = rawNearSemiringᵛ rawNearSemiring n + module RNS = RawNearSemiring nearSemiringᵛ open SemiringWithoutOneProperties semiringWithoutOne n public @@ -477,8 +471,8 @@ module SemiringWithoutAnnihilatingZeroProperties private module SWAZ = SemiringWithoutAnnihilatingZero semiringWithoutAnnihilatingZero - vecSemiring = rawSemiringᵛ rawSemiring n - module RS = RawSemiring vecSemiring + semiringᵛ = rawSemiringᵛ rawSemiring n + module RS = RawSemiring semiringᵛ open VecSemiringProperties rawSemiring n public open CommutativeMonoidProperties +-commutativeMonoid n public using (+ᴹ-isCommutativeMonoid) @@ -506,40 +500,40 @@ module SemiringProperties {a ℓ} (semiring : Semiring a ℓ) (n : ℕ) where module S = Semiring semiring private - vecNearSemiring = rawNearSemiringᵛ S.rawNearSemiring n - vecSemiring = rawSemiringᵛ S.rawSemiring n - module RNS = RawNearSemiring vecNearSemiring - module RS = RawSemiring vecSemiring - vecLeftSemi = rawLeftSemimoduleᵛ S.rawNearSemiring n - vecRightSemi = rawRightSemimoduleᵛ S.rawNearSemiring n - module LSM = RawLeftSemimodule vecLeftSemi - module RSM = RawRightSemimodule vecRightSemi + nearSemiringᵛ = rawNearSemiringᵛ S.rawNearSemiring n + semiringᵛ = rawSemiringᵛ S.rawSemiring n + module RNS = RawNearSemiring nearSemiringᵛ + module RS = RawSemiring semiringᵛ + leftSemiᵛ = rawLeftSemimoduleᵛ S.rawNearSemiring n + rightSemiᵛ = rawRightSemimoduleᵛ S.rawNearSemiring n + module LSM = RawLeftSemimodule leftSemiᵛ + module RSM = RawRightSemimodule rightSemiᵛ module RN = RawNearSemiringProperties semiring n isPreleftSemimodule : IsPreleftSemimodule semiring RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ - isPreleftSemimodule = RN.isPreleftSemimoduleVec + isPreleftSemimodule = RN.isPreleftSemimoduleᵛ isPrerightSemimodule : IsPrerightSemimodule semiring RNS._≈_ RNS._+_ RNS.0# RSM._*ᵣ_ - isPrerightSemimodule = RN.isPrerightSemimoduleVec + isPrerightSemimodule = RN.isPrerightSemimoduleᵛ isRightSemimodule : IsRightSemimodule semiring RNS._≈_ RNS._+_ RNS.0# RSM._*ᵣ_ isRightSemimodule = record - { +ᴹ-isCommutativeMonoid = IsBisemimodule.+ᴹ-isCommutativeMonoid RN.isBisemimoduleVec + { +ᴹ-isCommutativeMonoid = IsBisemimodule.+ᴹ-isCommutativeMonoid RN.isBisemimoduleᵛ ; isPrerightSemimodule = isPrerightSemimodule } isBisemimodule : IsBisemimodule semiring semiring RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ RSM._*ᵣ_ - isBisemimodule = RN.isBisemimoduleVec + isBisemimodule = RN.isBisemimoduleᵛ isLeftSemimodule : IsLeftSemimodule semiring RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ isLeftSemimodule = record - { +ᴹ-isCommutativeMonoid = IsBisemimodule.+ᴹ-isCommutativeMonoid RN.isBisemimoduleVec + { +ᴹ-isCommutativeMonoid = IsBisemimodule.+ᴹ-isCommutativeMonoid RN.isBisemimoduleᵛ ; isPreleftSemimodule = isPreleftSemimodule } +ᴹ-*-isSemiring : IsSemiring RS._≈_ RS._+_ RS._*_ RS.0# RS.1# - +ᴹ-*-isSemiring = RN.isSemiringVec + +ᴹ-*-isSemiring = RN.isSemiringᵛ leftSemimodule : LeftSemimodule _ _ _ leftSemimodule = record { isLeftSemimodule = isLeftSemimodule } @@ -555,10 +549,10 @@ module CommutativeSemiringProperties (commutativeSemiring : CommutativeSemiring module SR = RawSemiring rawSemiring baseNearSemiring = SR.rawNearSemiring - vecSemiring = rawSemiringᵛ rawSemiring n - vecNearSemiring = rawNearSemiringᵛ baseNearSemiring n - module RS = RawSemiring vecSemiring - module RNS = RawNearSemiring vecNearSemiring + semiringᵛ = rawSemiringᵛ rawSemiring n + nearSemiringᵛ = rawNearSemiringᵛ baseNearSemiring n + module RS = RawSemiring semiringᵛ + module RNS = RawNearSemiring nearSemiringᵛ module CS = CommutativeSemiring commutativeSemiring @@ -584,14 +578,14 @@ module RingWithoutOneProperties (ringWithoutOne : RingWithoutOne a ℓ) (n : ℕ baseNearSemiring = record { Carrier = Carrier ; _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; 0# = 0# } - vecNearSemiring = rawNearSemiringᵛ baseNearSemiring n - module RNS = RawNearSemiring vecNearSemiring + nearSemiringᵛ = rawNearSemiringᵛ baseNearSemiring n + module RNS = RawNearSemiring nearSemiringᵛ private module +G = Group +-group addRawGroup = +G.rawGroup - vecAddGroup = rawGroupᵛ addRawGroup n - module VG = RawGroup vecAddGroup + addGroupᵛ = rawGroupᵛ addRawGroup n + module VG = RawGroup addGroupᵛ open AbelianGroupProperties +-abelianGroup n using (+ᴹ-isAbelianGroup) public @@ -622,20 +616,20 @@ module RingProperties (ring : Ring a ℓ) (n : ℕ) where module SR = RawSemiring S.rawSemiring baseNearSemiring = SR.rawNearSemiring - vecNearSemiring = rawNearSemiringᵛ baseNearSemiring n - vecSemiring = rawSemiringᵛ S.rawSemiring n - module RNS = RawNearSemiring vecNearSemiring - module RS = RawSemiring vecSemiring + nearSemiringᵛ = rawNearSemiringᵛ baseNearSemiring n + semiringᵛ = rawSemiringᵛ S.rawSemiring n + module RNS = RawNearSemiring nearSemiringᵛ + module RS = RawSemiring semiringᵛ - vecLeftSemi = rawLeftSemimoduleᵛ baseNearSemiring n - vecRightSemi = rawRightSemimoduleᵛ baseNearSemiring n - module LSM = RawLeftSemimodule vecLeftSemi - module RSM = RawRightSemimodule vecRightSemi + leftSemiᵛ = rawLeftSemimoduleᵛ baseNearSemiring n + rightSemiᵛ = rawRightSemimoduleᵛ baseNearSemiring n + module LSM = RawLeftSemimodule leftSemiᵛ + module RSM = RawRightSemimodule rightSemiᵛ module +G = Group +-group addRawGroup = +G.rawGroup - vecAddGroup = rawGroupᵛ addRawGroup n - module VG = RawGroup vecAddGroup + addGroupᵛ = rawGroupᵛ addRawGroup n + module VG = RawGroup addGroupᵛ open SemiringProperties semiring n public open AbelianGroupProperties +-abelianGroup n public @@ -696,21 +690,21 @@ module CommutativeRingProperties (commutativeRing : CommutativeRing a ℓ) (n : module SR = RawSemiring S.rawSemiring baseNearSemiring = SR.rawNearSemiring - vecNearSemiring = rawNearSemiringᵛ baseNearSemiring n - vecSemiring = rawSemiringᵛ S.rawSemiring n + nearSemiringᵛ = rawNearSemiringᵛ baseNearSemiring n + semiringᵛ = rawSemiringᵛ S.rawSemiring n - module RNS = RawNearSemiring vecNearSemiring - module RS = RawSemiring vecSemiring + module RNS = RawNearSemiring nearSemiringᵛ + module RS = RawSemiring semiringᵛ - vecLeftSemi = rawLeftSemimoduleᵛ baseNearSemiring n - vecRightSemi = rawRightSemimoduleᵛ baseNearSemiring n - module LSM = RawLeftSemimodule vecLeftSemi - module RSM = RawRightSemimodule vecRightSemi + leftSemiᵛ = rawLeftSemimoduleᵛ baseNearSemiring n + rightSemiᵛ = rawRightSemimoduleᵛ baseNearSemiring n + module LSM = RawLeftSemimodule leftSemiᵛ + module RSM = RawRightSemimodule rightSemiᵛ module +G = Group Ri.+-group addRawGroup = +G.rawGroup - vecAddGroup = rawGroupᵛ addRawGroup n - module VG = RawGroup vecAddGroup + addGroupᵛ = rawGroupᵛ addRawGroup n + module VG = RawGroup addGroupᵛ open RingProperties ring n public @@ -721,10 +715,6 @@ module CommutativeRingProperties (commutativeRing : CommutativeRing a ℓ) (n : ; *-comm = λ xs ys i → *-comm (xs i) (ys i) } - private - *ₗ-*ᵣ-coincident : SimultaneousBiDefs.Coincident Carrier RNS._≈_ LSM._*ₗ_ RSM._*ᵣ_ - *ₗ-*ᵣ-coincident r xs i = *-comm r (xs i) - isModule : IsModule commutativeRing RNS._≈_ RNS._+_ RNS.0# VG._⁻¹ LSM._*ₗ_ RSM._*ᵣ_ isModule = record { isBimodule = isBimodule From e8de375cd93db208a171a7e2157a65f6042f6a4e Mon Sep 17 00:00:00 2001 From: e-mniang Date: Sun, 5 Oct 2025 13:13:24 -0400 Subject: [PATCH 4/4] applying the reviews --- src/Data/Vec/Functional/Algebra/Base.agda | 120 ++-- .../Vec/Functional/Algebra/Properties.agda | 648 +++++++++--------- 2 files changed, 365 insertions(+), 403 deletions(-) diff --git a/src/Data/Vec/Functional/Algebra/Base.agda b/src/Data/Vec/Functional/Algebra/Base.agda index 61d66b4d9d..2d960c87f3 100644 --- a/src/Data/Vec/Functional/Algebra/Base.agda +++ b/src/Data/Vec/Functional/Algebra/Base.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Some Vector-related module Definitions +-- Some VecF.Vector-related module Definitions ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} @@ -12,12 +12,12 @@ open import Level using (Level; suc; _⊔_) open import Function using (_$_) open import Data.Nat using (ℕ) open import Data.Fin using (Fin) -open import Data.Vec.Functional +import Data.Vec.Functional as VecF open import Algebra.Core open import Algebra.Bundles open import Algebra.Module open import Relation.Binary using (Rel) -open import Data.Vec.Functional.Relation.Binary.Pointwise using (Pointwise) +import Data.Vec.Functional.Relation.Binary.Pointwise as Pointwise private variable a ℓ : Level @@ -25,115 +25,103 @@ private variable n : ℕ ------------------------------------------------------------------------ --- Vector-lifted relations & operators +-- VecF.Vector-lifted raw structures -pointwiseᵛ : ( _≈_ : Rel A ℓ ) → Rel (Vector A n) ℓ -pointwiseᵛ _≈_ = Pointwise _≈_ - -zipWithᵛ : Op₂ A → Op₂ (Vector A n) -zipWithᵛ _∙_ = zipWith _∙_ - -mapᵛ : Op₁ A → Op₁ (Vector A n) -mapᵛ f = map f - ------------------------------------------------------------------------- --- Vector-lifted raw structures - -rawMagmaᵛ : RawMagma a ℓ → (n : ℕ) → RawMagma a ℓ -rawMagmaᵛ M n = +rawMagma : RawMagma a ℓ → (n : ℕ) → RawMagma a ℓ +rawMagma M n = record - { Carrier = Vector M.Carrier n - ; _≈_ = pointwiseᵛ M._≈_ - ; _∙_ = zipWithᵛ M._∙_ + { Carrier = VecF.Vector M.Carrier n + ; _≈_ = Pointwise.Pointwise M._≈_ + ; _∙_ = VecF.zipWith M._∙_ } where module M = RawMagma M -rawMonoidᵛ : RawMonoid a ℓ → (n : ℕ) → RawMonoid a ℓ -rawMonoidᵛ M n = +rawMonoid : RawMonoid a ℓ → (n : ℕ) → RawMonoid a ℓ +rawMonoid M n = record - { RawMagma (rawMagmaᵛ M.rawMagma n) + { RawMagma (rawMagma M.rawMagma n) ; ε = λ _ → M.ε } where module M = RawMonoid M -rawGroupᵛ : RawGroup a ℓ → (n : ℕ) → RawGroup a ℓ -rawGroupᵛ G n = +rawGroup : RawGroup a ℓ → (n : ℕ) → RawGroup a ℓ +rawGroup G n = record - { RawMonoid (rawMonoidᵛ G.rawMonoid n) - ; _⁻¹ = mapᵛ G._⁻¹ + { RawMonoid (rawMonoid G.rawMonoid n) + ; _⁻¹ = VecF.map G._⁻¹ } where module G = RawGroup G -rawNearSemiringᵛ : RawNearSemiring a ℓ → (n : ℕ) → RawNearSemiring a ℓ -rawNearSemiringᵛ NS n = +rawNearSemiring : RawNearSemiring a ℓ → (n : ℕ) → RawNearSemiring a ℓ +rawNearSemiring NS n = record - { Carrier = Vector NS.Carrier n - ; _≈_ = pointwiseᵛ NS._≈_ - ; _+_ = zipWithᵛ NS._+_ - ; _*_ = zipWithᵛ NS._*_ + { Carrier = VecF.Vector NS.Carrier n + ; _≈_ = Pointwise.Pointwise NS._≈_ + ; _+_ = VecF.zipWith NS._+_ + ; _*_ = VecF.zipWith NS._*_ ; 0# = λ _ → NS.0# } where module NS = RawNearSemiring NS -rawSemiringᵛ : RawSemiring a ℓ → (n : ℕ) → RawSemiring a ℓ -rawSemiringᵛ S n = +rawSemiring : RawSemiring a ℓ → (n : ℕ) → RawSemiring a ℓ +rawSemiring S n = record - { RawNearSemiring (rawNearSemiringᵛ S.rawNearSemiring n) + { RawNearSemiring (rawNearSemiring S.rawNearSemiring n) ; 1# = λ _ → S.1# } where module S = RawSemiring S -rawRingᵛ : RawRing a ℓ → (n : ℕ) → RawRing a ℓ -rawRingᵛ R n = +rawRing : RawRing a ℓ → (n : ℕ) → RawRing a ℓ +rawRing R n = record - { RawSemiring (rawSemiringᵛ R.rawSemiring n) - ; -_ = mapᵛ R.-_ + { RawSemiring (rawSemiring R.rawSemiring n) + ; -_ = VecF.map R.-_ } where module R = RawRing R ------------------------------------------------------------------------ --- Vector actions (left/right scalar multiplication) +-- VecF.Vector actions (left/right scalar multiplication) -_*ₗᵛ_ : {S : Set a} → Op₂ S → Opₗ S (Vector S n) -_*ₗᵛ_ _*_ r xs = map (r *_) xs +_*ₗ_ : {S : Set a} → Op₂ S → Opₗ S (VecF.Vector S n) +_*ₗ_ _*_ r xs = VecF.map (r *_) xs -_*ᵣᵛ_ : {S : Set a} → Op₂ S → Opᵣ S (Vector S n) -_*ᵣᵛ_ _*_ xs r = map (_* r) xs +_*ᵣ_ : {S : Set a} → Op₂ S → Opᵣ S (VecF.Vector S n) +_*ᵣ_ _*_ xs r = VecF.map (_* r) xs ------------------------------------------------------------------------ --- Vector-lifted semimodule bundles +-- VecF.Vector-lifted semimodule bundles -rawLeftSemimoduleᵛ : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawLeftSemimodule (RawNearSemiring.Carrier NS) a ℓ -rawLeftSemimoduleᵛ NS n = +rawLeftSemimodule : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawLeftSemimodule (RawNearSemiring.Carrier NS) a ℓ +rawLeftSemimodule NS n = record - { Carrierᴹ = Vector NS.Carrier n - ; _≈ᴹ_ = pointwiseᵛ NS._≈_ - ; _+ᴹ_ = zipWithᵛ NS._+_ - ; _*ₗ_ = _*ₗᵛ_ NS._*_ + { Carrierᴹ = VecF.Vector NS.Carrier n + ; _≈ᴹ_ = Pointwise.Pointwise NS._≈_ + ; _+ᴹ_ = VecF.zipWith NS._+_ + ; _*ₗ_ = _*ₗ_ NS._*_ ; 0ᴹ = λ _ → NS.0# } where module NS = RawNearSemiring NS -rawRightSemimoduleᵛ : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawRightSemimodule (RawNearSemiring.Carrier NS) a ℓ -rawRightSemimoduleᵛ NS n = +rawRightSemimodule : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawRightSemimodule (RawNearSemiring.Carrier NS) a ℓ +rawRightSemimodule NS n = record - { Carrierᴹ = Vector NS.Carrier n - ; _≈ᴹ_ = pointwiseᵛ NS._≈_ - ; _+ᴹ_ = zipWithᵛ NS._+_ - ; _*ᵣ_ = _*ᵣᵛ_ NS._*_ + { Carrierᴹ = VecF.Vector NS.Carrier n + ; _≈ᴹ_ = Pointwise.Pointwise NS._≈_ + ; _+ᴹ_ = VecF.zipWith NS._+_ + ; _*ᵣ_ = _*ᵣ_ NS._*_ ; 0ᴹ = λ _ → NS.0# } where module NS = RawNearSemiring NS -rawBisemimoduleᵛ : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawBisemimodule (RawNearSemiring.Carrier NS) +rawBisemimodule : (NS : RawNearSemiring a ℓ) (n : ℕ) → RawBisemimodule (RawNearSemiring.Carrier NS) (RawNearSemiring.Carrier NS) a ℓ -rawBisemimoduleᵛ NS n = +rawBisemimodule NS n = record - { Carrierᴹ = Vector NS.Carrier n - ; _≈ᴹ_ = pointwiseᵛ NS._≈_ - ; _+ᴹ_ = zipWithᵛ NS._+_ - ; _*ₗ_ = _*ₗᵛ_ NS._*_ - ; _*ᵣ_ = _*ᵣᵛ_ NS._*_ + { Carrierᴹ = VecF.Vector NS.Carrier n + ; _≈ᴹ_ = Pointwise.Pointwise NS._≈_ + ; _+ᴹ_ = VecF.zipWith NS._+_ + ; _*ₗ_ = _*ₗ_ NS._*_ + ; _*ᵣ_ = _*ᵣ_ NS._*_ ; 0ᴹ = λ _ → NS.0# } where module NS = RawNearSemiring NS \ No newline at end of file diff --git a/src/Data/Vec/Functional/Algebra/Properties.agda b/src/Data/Vec/Functional/Algebra/Properties.agda index deca24132a..0bde88682a 100644 --- a/src/Data/Vec/Functional/Algebra/Properties.agda +++ b/src/Data/Vec/Functional/Algebra/Properties.agda @@ -22,8 +22,8 @@ open import Algebra.Module.Structures open import Relation.Binary import Algebra.Definitions as Definitions open import Algebra.Structures -open import Data.Vec.Functional.Algebra.Base import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as Pointwise +import Data.Vec.Functional.Algebra.Base as V private variable a ℓ : Level @@ -33,72 +33,74 @@ private variable ------------------------------------------------------------------------ -- Raw structure properties -module RawMagmaProperties (rawMagma : RawMagma a ℓ) (n : ℕ) where - private - magmaᵛ = rawMagmaᵛ rawMagma n - module VM = RawMagma magmaᵛ - module M = RawMagma rawMagma - - open IsEquivalence +module RawMagmaProperties (M : RawMagma a ℓ) (n : ℕ) where + module VM = RawMagma (V.rawMagma M n) + module M = RawMagma M - isMagmaᵛ : IsMagma M._≈_ M._∙_ → IsMagma VM._≈_ VM._∙_ - isMagmaᵛ base = record + isMagma : IsMagma M._≈_ M._∙_ → IsMagma VM._≈_ VM._∙_ + isMagma base = record { isEquivalence = flip Pointwise.isEquivalence _ B.isEquivalence ; ∙-cong = λ x≈y u≈v i → B.∙-cong (x≈y i) (u≈v i) } where module B = IsMagma base - isCommutativeMagmaᵛ : IsCommutativeMagma M._≈_ M._∙_ → IsCommutativeMagma VM._≈_ VM._∙_ - isCommutativeMagmaᵛ base = record - { isMagma = isMagmaᵛ CM.isMagma - ; comm = λ xs ys i → CM.comm (xs i) (ys i) + isCommutativeMagma : + IsCommutativeMagma M._≈_ M._∙_ → + IsCommutativeMagma VM._≈_ VM._∙_ + isCommutativeMagma base = record + { isMagma = isMagma B.isMagma + ; comm = λ xs ys i → B.comm (xs i) (ys i) } - where module CM = IsCommutativeMagma base - - isSemigroupᵛ : IsSemigroup M._≈_ M._∙_ → IsSemigroup VM._≈_ VM._∙_ - isSemigroupᵛ base = record - { isMagma = isMagmaᵛ SG.isMagma - ; assoc = λ xs ys zs i → SG.assoc (xs i) (ys i) (zs i) + where module B = IsCommutativeMagma base + + isSemigroup : + IsSemigroup M._≈_ M._∙_ → + IsSemigroup VM._≈_ VM._∙_ + isSemigroup base = record + { isMagma = isMagma B.isMagma + ; assoc = λ xs ys zs i → B.assoc (xs i) (ys i) (zs i) } - where module SG = IsSemigroup base - - isCommutativeSemigroupᵛ : IsCommutativeSemigroup M._≈_ M._∙_ → IsCommutativeSemigroup VM._≈_ VM._∙_ - isCommutativeSemigroupᵛ base = record - { isSemigroup = isSemigroupᵛ CS.isSemigroup - ; comm = λ xs ys i → CS.comm (xs i) (ys i) + where module B = IsSemigroup base + + isCommutativeSemigroup : + IsCommutativeSemigroup M._≈_ M._∙_ → + IsCommutativeSemigroup VM._≈_ VM._∙_ + isCommutativeSemigroup base = record + { isSemigroup = isSemigroup B.isSemigroup + ; comm = λ xs ys i → B.comm (xs i) (ys i) } - where module CS = IsCommutativeSemigroup base + where module B = IsCommutativeSemigroup base ------------------------------------------------------------------------ -module RawMonoidProperties (rawMonoid : RawMonoid a ℓ) (n : ℕ) where - private - monoidᵛ = rawMonoidᵛ rawMonoid n - module VM = RawMonoid monoidᵛ - module RM = RawMonoid rawMonoid +module RawMonoidProperties (RM : RawMonoid a ℓ) (n : ℕ) where + module VMon = RawMonoid (V.rawMonoid RM n) + module RM = RawMonoid RM - open RawMagmaProperties (RawMonoid.rawMagma rawMonoid) n public + open RawMagmaProperties RM.rawMagma n public private - module ≈ = Definitions RM._≈_ - module ≈ᴹ = Definitions VM._≈_ + module ≈ = Definitions RM._≈_ + module ≈ᴹ = Definitions VMon._≈_ - +ᴹ-identityˡ : ≈.LeftIdentity RM.ε RM._∙_ → ≈ᴹ.LeftIdentity VM.ε VM._∙_ + +ᴹ-identityˡ : ≈.LeftIdentity RM.ε RM._∙_ → ≈ᴹ.LeftIdentity VMon.ε VMon._∙_ +ᴹ-identityˡ idˡ xs i = idˡ (xs i) - +ᴹ-identityʳ : ≈.RightIdentity RM.ε RM._∙_ → ≈ᴹ.RightIdentity VM.ε VM._∙_ + +ᴹ-identityʳ : ≈.RightIdentity RM.ε RM._∙_ → ≈ᴹ.RightIdentity VMon.ε VMon._∙_ +ᴹ-identityʳ idʳ xs i = idʳ (xs i) - +ᴹ-identity : ≈.Identity RM.ε RM._∙_ → ≈ᴹ.Identity VM.ε VM._∙_ + +ᴹ-identity : ≈.Identity RM.ε RM._∙_ → ≈ᴹ.Identity VMon.ε VMon._∙_ +ᴹ-identity (idˡ , idʳ) = +ᴹ-identityˡ idˡ , +ᴹ-identityʳ idʳ - isMonoidᵛ : IsMonoid RM._≈_ RM._∙_ RM.ε → IsMonoid VM._≈_ VM._∙_ VM.ε + isMonoidᵛ : IsMonoid RM._≈_ RM._∙_ RM.ε → IsMonoid VMon._≈_ VMon._∙_ VMon.ε isMonoidᵛ isMonoid = record - { isSemigroup = isSemigroupᵛ M.isSemigroup - ; identity = +ᴹ-identity M.identity - } where module M = IsMonoid isMonoid + { isSemigroup = isSemigroup Mon.isSemigroup + ; identity = +ᴹ-identity Mon.identity + } where module Mon = IsMonoid isMonoid - isCommutativeMonoidᵛ : IsCommutativeMonoid RM._≈_ RM._∙_ RM.ε → IsCommutativeMonoid VM._≈_ VM._∙_ VM.ε + isCommutativeMonoidᵛ : + IsCommutativeMonoid RM._≈_ RM._∙_ RM.ε → + IsCommutativeMonoid VMon._≈_ VMon._∙_ VMon.ε isCommutativeMonoidᵛ base = record { isMonoid = isMonoidᵛ CM.isMonoid ; comm = λ xs ys i → CM.comm (xs i) (ys i) @@ -106,37 +108,37 @@ module RawMonoidProperties (rawMonoid : RawMonoid a ℓ) (n : ℕ) where ------------------------------------------------------------------------ -module RawGroupProperties (rawGroup : RawGroup a ℓ) (n : ℕ) where +module RawGroupProperties (RG : RawGroup a ℓ) (n : ℕ) where private - groupᵛ = rawGroupᵛ rawGroup n - module RG = RawGroup groupᵛ - module G = RawGroup rawGroup - open RawMonoidProperties (RawGroup.rawMonoid rawGroup) n public + module VGp = RawGroup (V.rawGroup RG n) + module G = RawGroup RG + + open RawMonoidProperties G.rawMonoid n public private module ≈ = Definitions G._≈_ - module ≈ᴹ = Definitions RG._≈_ + module ≈ᴹ = Definitions VGp._≈_ - -ᴹ‿inverseˡ : ≈.LeftInverse G.ε G._⁻¹ G._∙_ → ≈ᴹ.LeftInverse RG.ε RG._⁻¹ RG._∙_ + -ᴹ‿inverseˡ : ≈.LeftInverse G.ε G._⁻¹ G._∙_ → ≈ᴹ.LeftInverse VGp.ε VGp._⁻¹ VGp._∙_ -ᴹ‿inverseˡ -‿inverseˡ xs i = -‿inverseˡ (xs i) - -ᴹ‿inverseʳ : ≈.RightInverse G.ε G._⁻¹ G._∙_ → ≈ᴹ.RightInverse RG.ε RG._⁻¹ RG._∙_ + -ᴹ‿inverseʳ : ≈.RightInverse G.ε G._⁻¹ G._∙_ → ≈ᴹ.RightInverse VGp.ε VGp._⁻¹ VGp._∙_ -ᴹ‿inverseʳ -‿inverseʳ xs i = -‿inverseʳ (xs i) - -ᴹ‿inverse : ≈.Inverse G.ε G._⁻¹ G._∙_ → ≈ᴹ.Inverse RG.ε RG._⁻¹ RG._∙_ + -ᴹ‿inverse : ≈.Inverse G.ε G._⁻¹ G._∙_ → ≈ᴹ.Inverse VGp.ε VGp._⁻¹ VGp._∙_ -ᴹ‿inverse (-‿inverseˡ , -‿inverseʳ) = -ᴹ‿inverseˡ -‿inverseˡ , -ᴹ‿inverseʳ -‿inverseʳ - -ᴹ‿cong : ≈.Congruent₁ G._⁻¹ → ≈ᴹ.Congruent₁ RG._⁻¹ + -ᴹ‿cong : ≈.Congruent₁ G._⁻¹ → ≈ᴹ.Congruent₁ VGp._⁻¹ -ᴹ‿cong -‿cong xs≈ys i = -‿cong (xs≈ys i) - isGroupᵛ : IsGroup G._≈_ G._∙_ G.ε G._⁻¹ → IsGroup RG._≈_ RG._∙_ RG.ε RG._⁻¹ + isGroupᵛ : IsGroup G._≈_ G._∙_ G.ε G._⁻¹ → IsGroup VGp._≈_ VGp._∙_ VGp.ε VGp._⁻¹ isGroupᵛ isGroup = record - { isMonoid = isMonoidᵛ M.isMonoid - ; inverse = -ᴹ‿inverse M.inverse - ; ⁻¹-cong = -ᴹ‿cong M.⁻¹-cong - } where module M = IsGroup isGroup + { isMonoid = isMonoidᵛ Gr.isMonoid + ; inverse = -ᴹ‿inverse Gr.inverse + ; ⁻¹-cong = -ᴹ‿cong Gr.⁻¹-cong + } where module Gr = IsGroup isGroup - isAbelianGroupᵛ : IsAbelianGroup G._≈_ G._∙_ G.ε G._⁻¹ → IsAbelianGroup RG._≈_ RG._∙_ RG.ε RG._⁻¹ + isAbelianGroupᵛ : IsAbelianGroup G._≈_ G._∙_ G.ε G._⁻¹ → IsAbelianGroup VGp._≈_ VGp._∙_ VGp.ε VGp._⁻¹ isAbelianGroupᵛ base = record { isGroup = isGroupᵛ AG.isGroup ; comm = λ xs ys i → AG.comm (xs i) (ys i) @@ -148,12 +150,12 @@ module RawGroupProperties (rawGroup : RawGroup a ℓ) (n : ℕ) where module VecSemiringProperties (rawSemiring : RawSemiring a ℓ) (n : ℕ) where private module SR = RawSemiring rawSemiring - rawNearSemiring = SR.rawNearSemiring - module NS = RawNearSemiring rawNearSemiring - nearSemiringᵛ = rawNearSemiringᵛ rawNearSemiring n + RNS = SR.rawNearSemiring + module NS = RawNearSemiring RNS + nearSemiringᵛ = V.rawNearSemiring RNS n module RNS = RawNearSemiring nearSemiringᵛ - leftSemiᵛ = rawLeftSemimoduleᵛ rawNearSemiring n - rightSemiᵛ = rawRightSemimoduleᵛ rawNearSemiring n + leftSemiᵛ = V.rawLeftSemimodule RNS n + rightSemiᵛ = V.rawRightSemimodule RNS n module LSM = RawLeftSemimodule leftSemiᵛ module RSM = RawRightSemimodule rightSemiᵛ @@ -175,48 +177,50 @@ module VecSemiringProperties (rawSemiring : RawSemiring a ℓ) (n : ℕ) where ------------------------------------------------------------------------ module RawNearSemiringProperties {ℓ ℓr} (R : Semiring ℓ ℓr) (n : ℕ) where - open Semiring R + module S = Semiring R private - module SR = RawSemiring rawSemiring - leftSemiᵛ = rawLeftSemimoduleᵛ rawNearSemiring n - rightSemiᵛ = rawRightSemimoduleᵛ rawNearSemiring n - module LSM = RawLeftSemimodule leftSemiᵛ - nearSemiringᵛ = rawNearSemiringᵛ rawNearSemiring n - module RNS = RawNearSemiring nearSemiringᵛ + module SR = RawSemiring S.rawSemiring + module NS = RawNearSemiring S.rawNearSemiring + + leftSemiᵛ = V.rawLeftSemimodule S.rawNearSemiring n + rightSemiᵛ = V.rawRightSemimodule S.rawNearSemiring n + nearSemiringᵛ = V.rawNearSemiring S.rawNearSemiring n + + module LSM = RawLeftSemimodule leftSemiᵛ module RSM = RawRightSemimodule rightSemiᵛ - module NS = RawNearSemiring rawNearSemiring + module RNS = RawNearSemiring nearSemiringᵛ - open RawMonoidProperties +-rawMonoid + open RawMonoidProperties S.+-rawMonoid n isPreleftSemimoduleᵛ : IsPreleftSemimodule R RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ isPreleftSemimoduleᵛ = record - { *ₗ-cong = λ x≈y u≈v i → *-cong x≈y (u≈v i) - ; *ₗ-zeroˡ = λ xs i → zeroˡ (xs i) - ; *ₗ-distribʳ = λ xs m n i → distribʳ (xs i) m n - ; *ₗ-identityˡ = λ xs i → *-identityˡ (xs i) - ; *ₗ-assoc = λ m n xs i → *-assoc m n (xs i) - ; *ₗ-zeroʳ = λ r i → zeroʳ r - ; *ₗ-distribˡ = λ m xs ys i → distribˡ m (xs i) (ys i) + { *ₗ-cong = λ x≈y u≈v i → S.*-cong x≈y (u≈v i) + ; *ₗ-zeroˡ = λ xs i → S.zeroˡ (xs i) + ; *ₗ-distribʳ = λ xs m n i → S.distribʳ (xs i) m n + ; *ₗ-identityˡ = λ xs i → S.*-identityˡ (xs i) + ; *ₗ-assoc = λ m n xs i → S.*-assoc m n (xs i) + ; *ₗ-zeroʳ = λ r i → S.zeroʳ r + ; *ₗ-distribˡ = λ m xs ys i → S.distribˡ m (xs i) (ys i) } isPrerightSemimoduleᵛ : IsPrerightSemimodule R RNS._≈_ RNS._+_ RNS.0# RSM._*ᵣ_ isPrerightSemimoduleᵛ = record - { *ᵣ-cong = λ x≈y u≈v i → *-cong (x≈y i) u≈v - ; *ᵣ-zeroʳ = λ xs i → zeroʳ (xs i) - ; *ᵣ-distribˡ = λ xs m n i → distribˡ (xs i) m n - ; *ᵣ-identityʳ = λ xs i → *-identityʳ (xs i) - ; *ᵣ-assoc = λ xs m n i → *-assoc (xs i) m n - ; *ᵣ-zeroˡ = λ r i → zeroˡ r - ; *ᵣ-distribʳ = λ xs m n i → distribʳ xs (m i) (n i) + { *ᵣ-cong = λ x≈y u≈v i → S.*-cong (x≈y i) u≈v + ; *ᵣ-zeroʳ = λ xs i → S.zeroʳ (xs i) + ; *ᵣ-distribˡ = λ xs m n i → S.distribˡ (xs i) m n + ; *ᵣ-identityʳ = λ xs i → S.*-identityʳ (xs i) + ; *ᵣ-assoc = λ xs m n i → S.*-assoc (xs i) m n + ; *ᵣ-zeroˡ = λ r i → S.zeroˡ r + ; *ᵣ-distribʳ = λ xs m n i → S.distribʳ xs (m i) (n i) } isBisemimoduleᵛ : IsBisemimodule R R RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ RSM._*ᵣ_ isBisemimoduleᵛ = record - { +ᴹ-isCommutativeMonoid = isCommutativeMonoidᵛ n +-isCommutativeMonoid + { +ᴹ-isCommutativeMonoid = isCommutativeMonoidᵛ S.+-isCommutativeMonoid ; isPreleftSemimodule = isPreleftSemimoduleᵛ ; isPrerightSemimodule = isPrerightSemimoduleᵛ - ; *ₗ-*ᵣ-assoc = λ xs m ys i → *-assoc xs (m i) ys + ; *ₗ-*ᵣ-assoc = λ xs m ys i → S.*-assoc xs (m i) ys } private @@ -229,141 +233,133 @@ module RawNearSemiringProperties {ℓ ℓr} (R : Semiring ℓ ℓr) (n : ℕ) wh isSemiringᵛ : IsSemiring RNS._≈_ RNS._+_ RNS._*_ RNS.0# 1#ᵛ isSemiringᵛ = record { isSemiringWithoutAnnihilatingZero = record - { +-isCommutativeMonoid = isCommutativeMonoidᵛ n +-isCommutativeMonoid - ; *-cong = λ x≈y u≈v → ( *-cong ∘ x≈y) ˢ u≈v - ; *-assoc = λ xs ys zs → ((*-assoc ∘ xs) ˢ ys) ˢ zs - ; *-identity = (λ xs → *-identityˡ ∘ xs) - , (λ xs → *-identityʳ ∘ xs) - ; distrib = (λ xs ys zs → ((distribˡ ∘ xs) ˢ ys) ˢ zs) - , (λ xs ys zs → ((distribʳ ∘ xs) ˢ ys) ˢ zs) + { +-isCommutativeMonoid = isCommutativeMonoidᵛ S.+-isCommutativeMonoid + ; *-cong = λ x≈y u≈v → ( S.*-cong ∘ x≈y) ˢ u≈v + ; *-assoc = λ xs ys zs → ((S.*-assoc ∘ xs) ˢ ys) ˢ zs + ; *-identity = (λ xs → S.*-identityˡ ∘ xs) + , (λ xs → S.*-identityʳ ∘ xs) + ; distrib = (λ xs ys zs → ((S.distribˡ ∘ xs) ˢ ys) ˢ zs) + , (λ xs ys zs → ((S.distribʳ ∘ xs) ˢ ys) ˢ zs) } - ; zero = (λ xs → zeroˡ ∘ xs) , (λ xs → zeroʳ ∘ xs) + ; zero = (λ xs → S.zeroˡ ∘ xs) , (λ xs → S.zeroʳ ∘ xs) } ------------------------------------------------------------------------ module MagmaProperties (magma : Magma a ℓ) (n : ℕ) where - open Magma magma using (_≈_; _∙_; isMagma; rawMagma) - private - magmaᵛ = rawMagmaᵛ rawMagma n - module VM = RawMagma magmaᵛ - module RM = RawMagma rawMagma + module Mg = Magma magma + module VM = RawMagma (V.rawMagma Mg.rawMagma n) + module RM = RawMagma Mg.rawMagma - open RawMagmaProperties rawMagma n public + open RawMagmaProperties Mg.rawMagma n public + renaming (isMagma to isMagmaᵛ) + hiding (module M; module VM) +ᴹ-isMagma : IsMagma VM._≈_ VM._∙_ - +ᴹ-isMagma = isMagmaᵛ isMagma + +ᴹ-isMagma = isMagmaᵛ Mg.isMagma +ᴹ-magma : Magma _ _ +ᴹ-magma = record { isMagma = +ᴹ-isMagma } ------------------------------------------------------------------------ -module CommutativeMagmaProperties (commutativeMagma : CommutativeMagma a ℓ) (n : ℕ) where - open CommutativeMagma commutativeMagma - private - magmaᵛ = rawMagmaᵛ rawMagma n - module VM = RawMagma magmaᵛ - module M = RawMagma rawMagma +module CommutativeMagmaProperties (cMag : CommutativeMagma a ℓ) (n : ℕ) where + module CM = CommutativeMagma cMag + module VM = RawMagma (V.rawMagma CM.rawMagma n) + module B = RawMagma CM.rawMagma - open MagmaProperties magma n public + open MagmaProperties CM.magma n public + renaming (isCommutativeMagma to isCommutativeMagmaᵛ) + hiding (module VM; module RM) +ᴹ-isCommutativeMagma : IsCommutativeMagma VM._≈_ VM._∙_ - +ᴹ-isCommutativeMagma = isCommutativeMagmaᵛ isCommutativeMagma + +ᴹ-isCommutativeMagma = isCommutativeMagmaᵛ CM.isCommutativeMagma +ᴹ-commutativeMagma : CommutativeMagma _ _ +ᴹ-commutativeMagma = record { isCommutativeMagma = +ᴹ-isCommutativeMagma } ------------------------------------------------------------------------ -module SemiRawGroupProperties (semigroup : Semigroup a ℓ) (n : ℕ) where - open Semigroup semigroup - - private - magmaᵛ = rawMagmaᵛ rawMagma n - module VM = RawMagma magmaᵛ - module M = RawMagma rawMagma +module SemiRawGroupProperties (sg : Semigroup a ℓ) (n : ℕ) where + module SG = Semigroup sg + module VM = RawMagma (V.rawMagma SG.rawMagma n) + module B = RawMagma SG.rawMagma - open MagmaProperties magma n public + open MagmaProperties SG.magma n public + renaming (isSemigroup to isSemigroupᵛ) + hiding (module VM; module RM) +ᴹ-isSemigroup : IsSemigroup VM._≈_ VM._∙_ - +ᴹ-isSemigroup = isSemigroupᵛ isSemigroup + +ᴹ-isSemigroup = isSemigroupᵛ SG.isSemigroup +ᴹ-semigroup : Semigroup _ _ +ᴹ-semigroup = record { isSemigroup = +ᴹ-isSemigroup } ------------------------------------------------------------------------ -module CommutativeSemigroupProperties (commutativeSemigroup : CommutativeSemigroup a ℓ) (n : ℕ) where - open CommutativeSemigroup commutativeSemigroup +module CommutativeSemigroupProperties (csg : CommutativeSemigroup a ℓ) (n : ℕ) where + module CS = CommutativeSemigroup csg + module VM = RawMagma (V.rawMagma CS.rawMagma n) + module B = RawMagma CS.rawMagma - private - magmaᵛ = rawMagmaᵛ rawMagma n - module VM = RawMagma magmaᵛ - module M = RawMagma rawMagma - - open MagmaProperties magma n public + open MagmaProperties CS.magma n public + renaming (isCommutativeSemigroup to isCommutativeSemigroupᵛ) + hiding (module VM; module RM) +ᴹ-isCommutativeSemigroup : IsCommutativeSemigroup VM._≈_ VM._∙_ - +ᴹ-isCommutativeSemigroup = isCommutativeSemigroupᵛ isCommutativeSemigroup + +ᴹ-isCommutativeSemigroup = isCommutativeSemigroupᵛ CS.isCommutativeSemigroup +ᴹ-commutativeSemigroup : CommutativeSemigroup _ _ +ᴹ-commutativeSemigroup = record { isCommutativeSemigroup = +ᴹ-isCommutativeSemigroup } ------------------------------------------------------------------------ -module MonoidProperties (monoid : Monoid a ℓ) (n : ℕ) where - open Monoid monoid - private - monoidᵛ = rawMonoidᵛ rawMonoid n - module VM = RawMonoid monoidᵛ - module M = RawMonoid rawMonoid +module MonoidProperties (mon : Monoid a ℓ) (n : ℕ) where + module M = Monoid mon + module VMon = RawMonoid (V.rawMonoid M.rawMonoid n) + module BaseMon = RawMonoid M.rawMonoid - open RawMonoidProperties rawMonoid n public using (+ᴹ-identity) - open SemiRawGroupProperties semigroup n public + open RawMonoidProperties M.rawMonoid n public using (+ᴹ-identity) + open SemiRawGroupProperties M.semigroup n public hiding (module B) - +ᴹ-isMonoid : IsMonoid VM._≈_ VM._∙_ VM.ε + +ᴹ-isMonoid : IsMonoid VMon._≈_ VMon._∙_ VMon.ε +ᴹ-isMonoid = record { isSemigroup = +ᴹ-isSemigroup - ; identity = +ᴹ-identity identity + ; identity = +ᴹ-identity M.identity } ------------------------------------------------------------------------- -module CommutativeMonoidProperties (commutativeMonoid : CommutativeMonoid a ℓ) (n : ℕ) where - open CommutativeMonoid commutativeMonoid +------------------------------------------------------------------------ - private - monoidᵛ = rawMonoidᵛ rawMonoid n - module VM = RawMonoid monoidᵛ - module M = RawMonoid rawMonoid +module CommutativeMonoidProperties (cMon : CommutativeMonoid a ℓ) (n : ℕ) where + module CM = CommutativeMonoid cMon + module VMonL = RawMonoid (V.rawMonoid CM.rawMonoid n) + module BaseMon = RawMonoid CM.rawMonoid - open RawMonoidProperties rawMonoid n + open RawMonoidProperties CM.rawMonoid n public - +ᴹ-isCommutativeMonoid : IsCommutativeMonoid VM._≈_ VM._∙_ VM.ε - +ᴹ-isCommutativeMonoid = isCommutativeMonoidᵛ isCommutativeMonoid + +ᴹ-isCommutativeMonoid : IsCommutativeMonoid VMonL._≈_ VMonL._∙_ VMonL.ε + +ᴹ-isCommutativeMonoid = isCommutativeMonoidᵛ CM.isCommutativeMonoid +ᴹ-commutativeMonoid : CommutativeMonoid _ _ +ᴹ-commutativeMonoid = record { isCommutativeMonoid = +ᴹ-isCommutativeMonoid } ------------------------------------------------------------------------- -module GroupProperties (group : Group a ℓ) (n : ℕ) where - open Group group +------------------------------------------------------------------------ - private - groupᵛ = rawGroupᵛ rawGroup n - module VG = RawGroup groupᵛ - module G = RawGroup rawGroup +module GroupProperties (grp : Group a ℓ) (n : ℕ) where + module G = Group grp + module VGrp = RawGroup (V.rawGroup G.rawGroup n) + module BaseG = RawGroup G.rawGroup - open RawGroupProperties rawGroup n public using (-ᴹ‿inverse; -ᴹ‿cong) - open MonoidProperties monoid n public + open RawGroupProperties G.rawGroup n public using (-ᴹ‿inverse; -ᴹ‿cong) + open MonoidProperties G.monoid n public - +ᴹ-isGroup : IsGroup VG._≈_ VG._∙_ VG.ε VG._⁻¹ + +ᴹ-isGroup : IsGroup VGrp._≈_ VGrp._∙_ VGrp.ε VGrp._⁻¹ +ᴹ-isGroup = record { isMonoid = +ᴹ-isMonoid - ; inverse = -ᴹ‿inverse inverse - ; ⁻¹-cong = -ᴹ‿cong ⁻¹-cong + ; inverse = -ᴹ‿inverse G.inverse + ; ⁻¹-cong = -ᴹ‿cong G.⁻¹-cong } +ᴹ-group : Group _ _ @@ -371,18 +367,16 @@ module GroupProperties (group : Group a ℓ) (n : ℕ) where ------------------------------------------------------------------------ -module AbelianGroupProperties (abelianGroup : AbelianGroup a ℓ) (n : ℕ) where - open AbelianGroup abelianGroup - private - groupᵛ = rawGroupᵛ rawGroup n - module VG = RawGroup groupᵛ +module AbelianGroupProperties (abg : AbelianGroup a ℓ) (n : ℕ) where + module AG = AbelianGroup abg + module VGroupL = RawGroup (V.rawGroup AG.rawGroup n) - open GroupProperties group n public + open GroupProperties AG.group n public - +ᴹ-isAbelianGroup : IsAbelianGroup VG._≈_ VG._∙_ VG.ε VG._⁻¹ + +ᴹ-isAbelianGroup : IsAbelianGroup VGroupL._≈_ VGroupL._∙_ VGroupL.ε VGroupL._⁻¹ +ᴹ-isAbelianGroup = record { isGroup = +ᴹ-isGroup - ; comm = λ xs ys i → comm (xs i) (ys i) + ; comm = λ xs ys i → AG.comm (xs i) (ys i) } +ᴹ-abelianGroup : AbelianGroup _ _ @@ -390,68 +384,66 @@ module AbelianGroupProperties (abelianGroup : AbelianGroup a ℓ) (n : ℕ) wher ------------------------------------------------------------------------ -module NearSemiringProperties (nearSemiring : NearSemiring a ℓ) (n : ℕ) where - open NearSemiring nearSemiring - private - module N = NearSemiring nearSemiring - nearSemiringᵛ = rawNearSemiringᵛ rawNearSemiring n - module RNS = RawNearSemiring nearSemiringᵛ +module NearSemiringProperties (near : NearSemiring a ℓ) (n : ℕ) where + module NS = NearSemiring near - open MonoidProperties +-monoid n public using (+ᴹ-isMonoid) + NSᵛ : RawNearSemiring a ℓ + NSᵛ = V.rawNearSemiring NS.rawNearSemiring n + module RNS = RawNearSemiring NSᵛ + + open MonoidProperties NS.+-monoid n public using (+ᴹ-isMonoid) +ᴹ-*-isNearSemiring : IsNearSemiring RNS._≈_ RNS._+_ RNS._*_ RNS.0# +ᴹ-*-isNearSemiring = record { +-isMonoid = +ᴹ-isMonoid - ; *-cong = λ x≈y u≈v i → N.*-cong (x≈y i) (u≈v i) - ; *-assoc = λ xs ys zs i → N.*-assoc (xs i) (ys i) (zs i) - ; distribʳ = λ xs ys zs i → N.distribʳ (xs i) (ys i) (zs i) - ; zeroˡ = λ xs i → N.zeroˡ (xs i) + ; *-cong = λ x≈y u≈v i → NS.*-cong (x≈y i) (u≈v i) + ; *-assoc = λ xs ys zs i → NS.*-assoc (xs i) (ys i) (zs i) + ; distribʳ = λ xs ys zs i → NS.distribʳ (xs i) (ys i) (zs i) + ; zeroˡ = λ xs i → NS.zeroˡ (xs i) } - +ᴹ-*-nearSemiring : NearSemiring _ _ +ᴹ-*-nearSemiring = record { isNearSemiring = +ᴹ-*-isNearSemiring } ------------------------------------------------------------------------ -module SemiringWithoutOneProperties (semiringWithoutOne : SemiringWithoutOne a ℓ) (n : ℕ) where - open SemiringWithoutOne semiringWithoutOne - private - nearSemiringᵛ = rawNearSemiringᵛ rawNearSemiring n - module RNS = RawNearSemiring nearSemiringᵛ - module SWO = SemiringWithoutOne semiringWithoutOne +module SemiringWithoutOneProperties (swo : SemiringWithoutOne a ℓ) (n : ℕ) where + module SWO = SemiringWithoutOne swo + module RNS = RawNearSemiring (V.rawNearSemiring SWO.rawNearSemiring n) - open CommutativeMonoidProperties +-commutativeMonoid n public using (+ᴹ-isCommutativeMonoid) + open CommutativeMonoidProperties SWO.+-commutativeMonoid n public + using (+ᴹ-isCommutativeMonoid) - +ᴹ-*-isSemiringWithoutOne : IsSemiringWithoutOne RNS._≈_ RNS._+_ RNS._*_ RNS.0# + +ᴹ-*-isSemiringWithoutOne : + IsSemiringWithoutOne RNS._≈_ RNS._+_ RNS._*_ RNS.0# +ᴹ-*-isSemiringWithoutOne = record { +-isCommutativeMonoid = +ᴹ-isCommutativeMonoid - ; *-cong = λ x≈y u≈v i → SWO.*-cong (x≈y i) (u≈v i) - ; *-assoc = λ xs ys zs i → SWO.*-assoc (xs i) (ys i) (zs i) - ; distrib = (λ xs ys zs i → proj₁ SWO.distrib (xs i) (ys i) (zs i)) , - (λ xs ys zs i → proj₂ SWO.distrib (xs i) (ys i) (zs i)) - ; zero = (λ xs i → proj₁ SWO.zero (xs i)) , - (λ xs i → proj₂ SWO.zero (xs i)) + ; *-cong = λ x≈y u≈v i → SWO.*-cong (x≈y i) (u≈v i) + ; *-assoc = λ xs ys zs i → SWO.*-assoc (xs i) (ys i) (zs i) + ; distrib = + (λ xs ys zs i → proj₁ SWO.distrib (xs i) (ys i) (zs i)) , + (λ xs ys zs i → proj₂ SWO.distrib (xs i) (ys i) (zs i)) + ; zero = + (λ xs i → proj₁ SWO.zero (xs i)) , + (λ xs i → proj₂ SWO.zero (xs i)) } +ᴹ-*-semiringWithoutOne : SemiringWithoutOne _ _ - +ᴹ-*-semiringWithoutOne = record { isSemiringWithoutOne = +ᴹ-*-isSemiringWithoutOne } + +ᴹ-*-semiringWithoutOne = record + { isSemiringWithoutOne = +ᴹ-*-isSemiringWithoutOne } ------------------------------------------------------------------------ module CommutativeSemiringWithoutOneProperties - (commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne a ℓ) (n : ℕ) where + (cswo : CommutativeSemiringWithoutOne a ℓ) (n : ℕ) where - open CommutativeSemiringWithoutOne commutativeSemiringWithoutOne - private - module CSWO = CommutativeSemiringWithoutOne commutativeSemiringWithoutOne - nearSemiringᵛ = rawNearSemiringᵛ rawNearSemiring n - module RNS = RawNearSemiring nearSemiringᵛ + module CSWO = CommutativeSemiringWithoutOne cswo + module VNS = RawNearSemiring (V.rawNearSemiring CSWO.rawNearSemiring n) - open SemiringWithoutOneProperties semiringWithoutOne n public + open SemiringWithoutOneProperties CSWO.semiringWithoutOne n public - +ᴹ-*-isCommutativeSemiringWithoutOne - : IsCommutativeSemiringWithoutOne RNS._≈_ RNS._+_ RNS._*_ RNS.0# + +ᴹ-*-isCommutativeSemiringWithoutOne : + IsCommutativeSemiringWithoutOne VNS._≈_ VNS._+_ VNS._*_ VNS.0# +ᴹ-*-isCommutativeSemiringWithoutOne = record { isSemiringWithoutOne = +ᴹ-*-isSemiringWithoutOne ; *-comm = λ xs ys i → CSWO.*-comm (xs i) (ys i) @@ -464,28 +456,25 @@ module CommutativeSemiringWithoutOneProperties ------------------------------------------------------------------------ module SemiringWithoutAnnihilatingZeroProperties - (semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero a ℓ) + (swaz : SemiringWithoutAnnihilatingZero a ℓ) (n : ℕ) where - open SemiringWithoutAnnihilatingZero semiringWithoutAnnihilatingZero - private - module SWAZ = SemiringWithoutAnnihilatingZero semiringWithoutAnnihilatingZero - - semiringᵛ = rawSemiringᵛ rawSemiring n - module RS = RawSemiring semiringᵛ + module SWAZ = SemiringWithoutAnnihilatingZero swaz + module RSv = RawSemiring (V.rawSemiring SWAZ.rawSemiring n) - open VecSemiringProperties rawSemiring n public - open CommutativeMonoidProperties +-commutativeMonoid n public using (+ᴹ-isCommutativeMonoid) + open VecSemiringProperties SWAZ.rawSemiring n public + open CommutativeMonoidProperties SWAZ.+-commutativeMonoid n public + using (+ᴹ-isCommutativeMonoid) +ᴹ-*-isSemiringWithoutAnnihilatingZero - : IsSemiringWithoutAnnihilatingZero RS._≈_ RS._+_ RS._*_ RS.0# RS.1# + : IsSemiringWithoutAnnihilatingZero RSv._≈_ RSv._+_ RSv._*_ RSv.0# RSv.1# +ᴹ-*-isSemiringWithoutAnnihilatingZero = record { +-isCommutativeMonoid = +ᴹ-isCommutativeMonoid ; *-cong = λ x≈y u≈v i → SWAZ.*-cong (x≈y i) (u≈v i) ; *-assoc = λ xs ys zs i → SWAZ.*-assoc (xs i) (ys i) (zs i) ; *-identity = let idˡ , idʳ = SWAZ.*-identity in (λ xs i → idˡ (xs i)) , (λ xs i → idʳ (xs i)) - ; distrib = let dˡ , dʳ = SWAZ.distrib in + ; distrib = let dˡ , dʳ = SWAZ.distrib in (λ xs ys zs i → dˡ (xs i) (ys i) (zs i)) , (λ xs ys zs i → dʳ (xs i) (ys i) (zs i)) } @@ -500,35 +489,38 @@ module SemiringProperties {a ℓ} (semiring : Semiring a ℓ) (n : ℕ) where module S = Semiring semiring private - nearSemiringᵛ = rawNearSemiringᵛ S.rawNearSemiring n - semiringᵛ = rawSemiringᵛ S.rawSemiring n - module RNS = RawNearSemiring nearSemiringᵛ - module RS = RawSemiring semiringᵛ - leftSemiᵛ = rawLeftSemimoduleᵛ S.rawNearSemiring n - rightSemiᵛ = rawRightSemimoduleᵛ S.rawNearSemiring n - module LSM = RawLeftSemimodule leftSemiᵛ - module RSM = RawRightSemimodule rightSemiᵛ + module RNS = RawNearSemiring (V.rawNearSemiring S.rawNearSemiring n) + module RS = RawSemiring (V.rawSemiring S.rawSemiring n) + module LSM = RawLeftSemimodule (V.rawLeftSemimodule S.rawNearSemiring n) + module RSM = RawRightSemimodule (V.rawRightSemimodule S.rawNearSemiring n) - module RN = RawNearSemiringProperties semiring n + module RN = RawNearSemiringProperties semiring n - isPreleftSemimodule : IsPreleftSemimodule semiring RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ + isPreleftSemimodule : + IsPreleftSemimodule semiring RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ isPreleftSemimodule = RN.isPreleftSemimoduleᵛ - isPrerightSemimodule : IsPrerightSemimodule semiring RNS._≈_ RNS._+_ RNS.0# RSM._*ᵣ_ + isPrerightSemimodule : + IsPrerightSemimodule semiring RNS._≈_ RNS._+_ RNS.0# RSM._*ᵣ_ isPrerightSemimodule = RN.isPrerightSemimoduleᵛ - isRightSemimodule : IsRightSemimodule semiring RNS._≈_ RNS._+_ RNS.0# RSM._*ᵣ_ + isRightSemimodule : + IsRightSemimodule semiring RNS._≈_ RNS._+_ RNS.0# RSM._*ᵣ_ isRightSemimodule = record - { +ᴹ-isCommutativeMonoid = IsBisemimodule.+ᴹ-isCommutativeMonoid RN.isBisemimoduleᵛ + { +ᴹ-isCommutativeMonoid = + IsBisemimodule.+ᴹ-isCommutativeMonoid RN.isBisemimoduleᵛ ; isPrerightSemimodule = isPrerightSemimodule } - isBisemimodule : IsBisemimodule semiring semiring RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ RSM._*ᵣ_ + isBisemimodule : + IsBisemimodule semiring semiring RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ RSM._*ᵣ_ isBisemimodule = RN.isBisemimoduleᵛ - isLeftSemimodule : IsLeftSemimodule semiring RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ + isLeftSemimodule : + IsLeftSemimodule semiring RNS._≈_ RNS._+_ RNS.0# LSM._*ₗ_ isLeftSemimodule = record - { +ᴹ-isCommutativeMonoid = IsBisemimodule.+ᴹ-isCommutativeMonoid RN.isBisemimoduleᵛ + { +ᴹ-isCommutativeMonoid = + IsBisemimodule.+ᴹ-isCommutativeMonoid RN.isBisemimoduleᵛ ; isPreleftSemimodule = isPreleftSemimodule } @@ -541,64 +533,62 @@ module SemiringProperties {a ℓ} (semiring : Semiring a ℓ) (n : ℕ) where +ᴹ-*-semiring : Semiring _ _ +ᴹ-*-semiring = record { isSemiring = +ᴹ-*-isSemiring } ------------------------------------------------------------------------- -module CommutativeSemiringProperties (commutativeSemiring : CommutativeSemiring a ℓ) (n : ℕ) where - open CommutativeSemiring commutativeSemiring - private - module SR = RawSemiring rawSemiring - baseNearSemiring = SR.rawNearSemiring +------------------------------------------------------------------------ - semiringᵛ = rawSemiringᵛ rawSemiring n - nearSemiringᵛ = rawNearSemiringᵛ baseNearSemiring n - module RS = RawSemiring semiringᵛ - module RNS = RawNearSemiring nearSemiringᵛ +module CommutativeSemiringProperties + (cSem : CommutativeSemiring a ℓ) (n : ℕ) where - module CS = CommutativeSemiring commutativeSemiring + module CS = CommutativeSemiring cSem + module RSv = RawSemiring (V.rawSemiring CS.rawSemiring n) - open SemiringProperties semiring n public + open SemiringProperties CS.semiring n public - +ᴹ-*-isCommutativeSemiring : IsCommutativeSemiring RS._≈_ RS._+_ RS._*_ RS.0# RS.1# + +ᴹ-*-isCommutativeSemiring : + IsCommutativeSemiring RSv._≈_ RSv._+_ RSv._*_ RSv.0# RSv.1# +ᴹ-*-isCommutativeSemiring = record { isSemiring = +ᴹ-*-isSemiring ; *-comm = λ xs ys i → CS.*-comm (xs i) (ys i) } +ᴹ-*-commutativeSemiring : CommutativeSemiring _ _ - +ᴹ-*-commutativeSemiring = record - { isCommutativeSemiring = +ᴹ-*-isCommutativeSemiring } + +ᴹ-*-commutativeSemiring = + record { isCommutativeSemiring = +ᴹ-*-isCommutativeSemiring } ------------------------------------------------------------------------ -module RingWithoutOneProperties (ringWithoutOne : RingWithoutOne a ℓ) (n : ℕ) where - open RingWithoutOne ringWithoutOne +module RingWithoutOneProperties (rwo : RingWithoutOne a ℓ) (n : ℕ) where + module RW = RingWithoutOne rwo private baseNearSemiring : RawNearSemiring a ℓ baseNearSemiring = record - { Carrier = Carrier ; _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; 0# = 0# } + { Carrier = RW.Carrier + ; _≈_ = RW._≈_ + ; _+_ = RW._+_ + ; _*_ = RW._*_ + ; 0# = RW.0# + } - nearSemiringᵛ = rawNearSemiringᵛ baseNearSemiring n - module RNS = RawNearSemiring nearSemiringᵛ + module RNS = RawNearSemiring (V.rawNearSemiring baseNearSemiring n) private - module +G = Group +-group - addRawGroup = +G.rawGroup - addGroupᵛ = rawGroupᵛ addRawGroup n - module VG = RawGroup addGroupᵛ + module +G = Group RW.+-group + addRawGroup = +G.rawGroup + module VG = RawGroup (V.rawGroup addRawGroup n) - open AbelianGroupProperties +-abelianGroup n using (+ᴹ-isAbelianGroup) public + open AbelianGroupProperties RW.+-abelianGroup n using (+ᴹ-isAbelianGroup) public private - module RW1 = IsRingWithoutOne (RingWithoutOne.isRingWithoutOne ringWithoutOne) + module IW1 = IsRingWithoutOne RW.isRingWithoutOne - +ᴹ-*-isRingWithoutOne - : IsRingWithoutOne RNS._≈_ RNS._+_ RNS._*_ VG._⁻¹ RNS.0# + +ᴹ-*-isRingWithoutOne : + IsRingWithoutOne RNS._≈_ RNS._+_ RNS._*_ VG._⁻¹ RNS.0# +ᴹ-*-isRingWithoutOne = record { +-isAbelianGroup = +ᴹ-isAbelianGroup - ; *-cong = λ x≈y u≈v i → RW1.*-cong (x≈y i) (u≈v i) - ; *-assoc = λ xs ys zs i → RW1.*-assoc (xs i) (ys i) (zs i) - ; distrib = let dₗ , dᵣ = RW1.distrib in + ; *-cong = λ x≈y u≈v i → IW1.*-cong (x≈y i) (u≈v i) + ; *-assoc = λ xs ys zs i → IW1.*-assoc (xs i) (ys i) (zs i) + ; distrib = let dₗ , dᵣ = IW1.distrib in (λ xs ys zs i → dₗ (xs i) (ys i) (zs i)) , (λ xs ys zs i → dᵣ (xs i) (ys i) (zs i)) } @@ -609,67 +599,60 @@ module RingWithoutOneProperties (ringWithoutOne : RingWithoutOne a ℓ) (n : ℕ ------------------------------------------------------------------------ module RingProperties (ring : Ring a ℓ) (n : ℕ) where - open Ring ring - + module Rg = Ring ring private - module S = Semiring semiring - module SR = RawSemiring S.rawSemiring - baseNearSemiring = SR.rawNearSemiring - - nearSemiringᵛ = rawNearSemiringᵛ baseNearSemiring n - semiringᵛ = rawSemiringᵛ S.rawSemiring n - module RNS = RawNearSemiring nearSemiringᵛ - module RS = RawSemiring semiringᵛ - - leftSemiᵛ = rawLeftSemimoduleᵛ baseNearSemiring n - rightSemiᵛ = rawRightSemimoduleᵛ baseNearSemiring n - module LSM = RawLeftSemimodule leftSemiᵛ - module RSM = RawRightSemimodule rightSemiᵛ - - module +G = Group +-group - addRawGroup = +G.rawGroup - addGroupᵛ = rawGroupᵛ addRawGroup n - module VG = RawGroup addGroupᵛ - - open SemiringProperties semiring n public - open AbelianGroupProperties +-abelianGroup n public + module S = Semiring Rg.semiring + module RNSv = RawNearSemiring (V.rawNearSemiring S.rawNearSemiring n) + module RSv = RawSemiring (V.rawSemiring S.rawSemiring n) + module LSMv = RawLeftSemimodule (V.rawLeftSemimodule S.rawNearSemiring n) + module RSMv = RawRightSemimodule (V.rawRightSemimodule S.rawNearSemiring n) + module +G = Group Rg.+-group + module VGrp = RawGroup (V.rawGroup +G.rawGroup n) + + open SemiringProperties Rg.semiring n public + open AbelianGroupProperties Rg.+-abelianGroup n public using (+ᴹ-isAbelianGroup; -ᴹ‿cong; -ᴹ‿inverse) - isRightModule : IsRightModule ring RNS._≈_ RNS._+_ RNS.0# VG._⁻¹ RSM._*ᵣ_ + isRightModule : + IsRightModule ring RNSv._≈_ RNSv._+_ RNSv.0# VGrp._⁻¹ RSMv._*ᵣ_ isRightModule = record { isRightSemimodule = isRightSemimodule - ; -ᴹ‿cong = -ᴹ‿cong -‿cong - ; -ᴹ‿inverse = -ᴹ‿inverse -‿inverse + ; -ᴹ‿cong = -ᴹ‿cong Rg.-‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse Rg.-‿inverse } - isBimodule : IsBimodule ring ring RNS._≈_ RNS._+_ RNS.0# VG._⁻¹ LSM._*ₗ_ RSM._*ᵣ_ + isBimodule : + IsBimodule ring ring RNSv._≈_ RNSv._+_ RNSv.0# VGrp._⁻¹ LSMv._*ₗ_ RSMv._*ᵣ_ isBimodule = record { isBisemimodule = isBisemimodule - ; -ᴹ‿cong = -ᴹ‿cong -‿cong - ; -ᴹ‿inverse = -ᴹ‿inverse -‿inverse + ; -ᴹ‿cong = -ᴹ‿cong Rg.-‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse Rg.-‿inverse } - isLeftModule : IsLeftModule ring RNS._≈_ RNS._+_ RNS.0# VG._⁻¹ LSM._*ₗ_ + isLeftModule : + IsLeftModule ring RNSv._≈_ RNSv._+_ RNSv.0# VGrp._⁻¹ LSMv._*ₗ_ isLeftModule = record { isLeftSemimodule = isLeftSemimodule - ; -ᴹ‿cong = -ᴹ‿cong -‿cong - ; -ᴹ‿inverse = -ᴹ‿inverse -‿inverse + ; -ᴹ‿cong = -ᴹ‿cong Rg.-‿cong + ; -ᴹ‿inverse = -ᴹ‿inverse Rg.-‿inverse } - +ᴹ-*-isRing : IsRing RS._≈_ RS._+_ RS._*_ VG._⁻¹ RS.0# RS.1# + +ᴹ-*-isRing : IsRing RSv._≈_ RSv._+_ RSv._*_ VGrp._⁻¹ RSv.0# RSv.1# +ᴹ-*-isRing = record { +-isAbelianGroup = +ᴹ-isAbelianGroup - ; *-cong = λ x≈y u≈v i → *-cong (x≈y i) (u≈v i) - ; *-assoc = λ xs ys zs i → *-assoc (xs i) (ys i) (zs i) - ; *-identity = let idₗ , idᵣ = *-identity in - (λ xs i → idₗ (xs i)) , (λ xs i → idᵣ (xs i)) - ; distrib = let dₗ , dᵣ = distrib in - (λ xs ys zs i → dₗ (xs i) (ys i) (zs i)) - , (λ xs ys zs i → dᵣ (xs i) (ys i) (zs i)) + ; *-cong = λ x≈y u≈v i → Rg.*-cong (x≈y i) (u≈v i) + ; *-assoc = λ xs ys zs i → Rg.*-assoc (xs i) (ys i) (zs i) + ; *-identity = + let idₗ , idᵣ = Rg.*-identity in + (λ xs i → idₗ (xs i)) , (λ xs i → idᵣ (xs i)) + ; distrib = + let dₗ , dᵣ = Rg.distrib in + (λ xs ys zs i → dₗ (xs i) (ys i) (zs i)) , + (λ xs ys zs i → dᵣ (xs i) (ys i) (zs i)) } - leftModule : LeftModule _ _ _ - leftModule = record { isLeftModule = isLeftModule } + leftModule : LeftModule _ _ _ + leftModule = record { isLeftModule = isLeftModule } bisemimodule : Bisemimodule _ _ _ _ bisemimodule = record { isBisemimodule = isBisemimodule } @@ -677,49 +660,40 @@ module RingProperties (ring : Ring a ℓ) (n : ℕ) where rightModule : RightModule _ _ _ rightModule = record { isRightModule = isRightModule } - bimodule : Bimodule _ _ _ _ - bimodule = record { isBimodule = isBimodule } + bimodule : Bimodule _ _ _ _ + bimodule = record { isBimodule = isBimodule } ------------------------------------------------------------------------ -module CommutativeRingProperties (commutativeRing : CommutativeRing a ℓ) (n : ℕ) where - open CommutativeRing commutativeRing - private - module Ri = Ring ring - module S = Semiring Ri.semiring - module SR = RawSemiring S.rawSemiring - baseNearSemiring = SR.rawNearSemiring +module CommutativeRingProperties (cRing : CommutativeRing a ℓ) (n : ℕ) where + module CR = CommutativeRing cRing - nearSemiringᵛ = rawNearSemiringᵛ baseNearSemiring n - semiringᵛ = rawSemiringᵛ S.rawSemiring n + module Ri = Ring CR.ring + module Sem = Semiring Ri.semiring - module RNS = RawNearSemiring nearSemiringᵛ - module RS = RawSemiring semiringᵛ + module RNSv = RawNearSemiring (V.rawNearSemiring Sem.rawNearSemiring n) + module RSv = RawSemiring (V.rawSemiring Sem.rawSemiring n) + module LSMv = RawLeftSemimodule (V.rawLeftSemimodule Sem.rawNearSemiring n) + module RSMv = RawRightSemimodule (V.rawRightSemimodule Sem.rawNearSemiring n) - leftSemiᵛ = rawLeftSemimoduleᵛ baseNearSemiring n - rightSemiᵛ = rawRightSemimoduleᵛ baseNearSemiring n - module LSM = RawLeftSemimodule leftSemiᵛ - module RSM = RawRightSemimodule rightSemiᵛ - - module +G = Group Ri.+-group - addRawGroup = +G.rawGroup - addGroupᵛ = rawGroupᵛ addRawGroup n - module VG = RawGroup addGroupᵛ + module +G = Group Ri.+-group + module VGrp = RawGroup (V.rawGroup +G.rawGroup n) - open RingProperties ring n public + open RingProperties CR.ring n public - +ᴹ-*-isCommutativeRing - : IsCommutativeRing RS._≈_ RS._+_ RS._*_ VG._⁻¹ RS.0# RS.1# + +ᴹ-*-isCommutativeRing : + IsCommutativeRing RSv._≈_ RSv._+_ RSv._*_ VGrp._⁻¹ RSv.0# RSv.1# +ᴹ-*-isCommutativeRing = record { isRing = +ᴹ-*-isRing - ; *-comm = λ xs ys i → *-comm (xs i) (ys i) + ; *-comm = λ xs ys i → CR.*-comm (xs i) (ys i) } - isModule : IsModule commutativeRing RNS._≈_ RNS._+_ RNS.0# VG._⁻¹ LSM._*ₗ_ RSM._*ᵣ_ + isModule : + IsModule cRing RNSv._≈_ RNSv._+_ RNSv.0# VGrp._⁻¹ LSMv._*ₗ_ RSMv._*ᵣ_ isModule = record - { isBimodule = isBimodule - ; *ₗ-*ᵣ-coincident = λ r xs i → *-comm r (xs i) + { isBimodule = isBimodule + ; *ₗ-*ᵣ-coincident = λ r xs i → CR.*-comm r (xs i) } - module' : Module _ _ _ - module' = record { isModule = isModule } \ No newline at end of file + ⟨module⟩ : Module _ _ _ + ⟨module⟩ = record { isModule = isModule }