diff --git a/src/Algebra/Action/Bundles.agda b/src/Algebra/Action/Bundles.agda new file mode 100644 index 0000000000..d31b0a543e --- /dev/null +++ b/src/Algebra/Action/Bundles.agda @@ -0,0 +1,137 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Setoid Actions and Monoid Actions +------------------------------------------------------------------------ + +------------------------------------------------------------------------ +-- Currently, this module (attempts to) systematically distinguish +-- between left- and right- actions, but unfortunately, trying to avoid +-- long names such as `Algebra.Action.Bundles.MonoidAction.LeftAction` +-- leads to the possibly/probably suboptimal use of `Left` and `Right` as +-- submodule names, when these are intended only to be used qualified by +-- the type of Action to which they refer, eg. as MonoidAction.Left etc. +------------------------------------------------------------------------ + + +{-# OPTIONS --cubical-compatible --safe #-} + +module Algebra.Action.Bundles where + +import Algebra.Action.Definitions as Definitions +open import Algebra.Action.Structures using (IsLeftAction; IsRightAction) +open import Algebra.Bundles using (Magma; Monoid) +open import Level using (Level; _⊔_) +open import Data.List.Base using ([]; _++_) +import Data.List.Relation.Binary.Equality.Setoid as ≋ +open import Relation.Binary.Bundles using (Setoid) + +private + variable + a c r ℓ : Level + + +------------------------------------------------------------------------ +-- Basic definition: a Setoid action yields underlying action structure + +module SetoidAction (S : Setoid c ℓ) (A : Setoid a r) where + + private + + module S = Setoid S + module A = Setoid A + + open ≋ S using (≋-refl) + + record Left : Set (a ⊔ r ⊔ c ⊔ ℓ) where + + field + isLeftAction : IsLeftAction S._≈_ A._≈_ + + open IsLeftAction isLeftAction public + + ▷-congˡ : ∀ {m x y} → x A.≈ y → m ▷ x A.≈ m ▷ y + ▷-congˡ x≈y = ▷-cong S.refl x≈y + + ▷-congʳ : ∀ {m n x} → m S.≈ n → m ▷ x A.≈ n ▷ x + ▷-congʳ m≈n = ▷-cong m≈n A.refl + + []-act : ∀ x → [] ▷⋆ x A.≈ x + []-act _ = []-act-cong A.refl + + ++-act : ∀ ms ns x → (ms ++ ns) ▷⋆ x A.≈ ms ▷⋆ ns ▷⋆ x + ++-act ms ns x = ++-act-cong ms ≋-refl A.refl + + record Right : Set (a ⊔ r ⊔ c ⊔ ℓ) where + + field + isRightAction : IsRightAction S._≈_ A._≈_ + + open IsRightAction isRightAction public + + ◁-congˡ : ∀ {x y m} → x A.≈ y → x ◁ m A.≈ y ◁ m + ◁-congˡ x≈y = ◁-cong x≈y S.refl + + ◁-congʳ : ∀ {m n x} → m S.≈ n → x ◁ m A.≈ x ◁ n + ◁-congʳ m≈n = ◁-cong A.refl m≈n + + ++-act : ∀ x ms ns → x ◁⋆ (ms ++ ns) A.≈ x ◁⋆ ms ◁⋆ ns + ++-act x ms ns = ++-act-cong A.refl ms ≋-refl + + []-act : ∀ x → x ◁⋆ [] A.≈ x + []-act x = []-act-cong A.refl + + +------------------------------------------------------------------------ +-- Definitions: indexed over an underlying SetoidAction + +module MagmaAction (M : Magma c ℓ) (A : Setoid a r) where + + private + + open module M = Magma M using (_∙_; setoid) + open module A = Setoid A using (_≈_) + open Definitions M._≈_ _≈_ + + record Left (leftAction : SetoidAction.Left setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ) + where + + open SetoidAction.Left leftAction public + + field + ∙-act : IsActionˡ _▷_ _∙_ + + record Right (rightAction : SetoidAction.Right setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ) + where + + open SetoidAction.Right rightAction public + + field + ∙-act : IsActionʳ _◁_ _∙_ + + +module MonoidAction (M : Monoid c ℓ) (A : Setoid a r) where + + private + + open module M = Monoid M using (ε; _∙_; setoid) + open module A = Setoid A using (_≈_) + open Definitions M._≈_ _≈_ + + record Left (leftAction : SetoidAction.Left setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ) + where + + open SetoidAction.Left leftAction public + + field + ∙-act : IsActionˡ _▷_ _∙_ + ε-act : IsIdentityˡ _▷_ ε + + record Right (rightAction : SetoidAction.Right setoid A) : Set (a ⊔ r ⊔ c ⊔ ℓ) + where + + open SetoidAction.Right rightAction public + + field + ∙-act : IsActionʳ _◁_ _∙_ + ε-act : IsIdentityʳ _◁_ ε diff --git a/src/Algebra/Action/Construct/FreeMonoid.agda b/src/Algebra/Action/Construct/FreeMonoid.agda new file mode 100644 index 0000000000..a1770250fe --- /dev/null +++ b/src/Algebra/Action/Construct/FreeMonoid.agda @@ -0,0 +1,70 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- The free MonoidAction on a SetoidAction, arising from ListAction +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Relation.Binary.Bundles using (Setoid) + +module Algebra.Action.Construct.FreeMonoid + {a c r ℓ} (S : Setoid c ℓ) (A : Setoid a r) + where + +open import Algebra.Action.Bundles +open import Algebra.Action.Structures using (IsLeftAction; IsRightAction) +open import Algebra.Bundles using (Monoid) + +open import Data.List.Relation.Binary.Equality.Setoid.Properties S using (monoid) + + +------------------------------------------------------------------------ +-- A Setoid action yields an iterated ListS action, which is +-- the underlying SetoidAction of the FreeMonoid construction + +module SetoidActions where + + open SetoidAction + open Monoid monoid using (setoid) + + leftAction : (left : Left S A) → Left setoid A + leftAction left = record + { isLeftAction = record + { _▷_ = _▷⋆_ + ; ▷-cong = ▷⋆-cong + } + } + where open Left left + + rightAction : (right : Right S A) → Right setoid A + rightAction right = record + { isRightAction = record + { _◁_ = _◁⋆_ + ; ◁-cong = ◁⋆-cong + } + } + where open Right right + + +------------------------------------------------------------------------ +-- Now: define the MonoidActions of the (Monoid based on) ListS on A + +module MonoidActions where + + open MonoidAction monoid A + + leftAction : (left : SetoidAction.Left S A) → Left (SetoidActions.leftAction left) + leftAction left = record + { ∙-act = ++-act + ; ε-act = []-act + } + where open SetoidAction.Left left + + rightAction : (right : SetoidAction.Right S A) → Right (SetoidActions.rightAction right) + rightAction right = record + { ∙-act = ++-act + ; ε-act = []-act + } + where open SetoidAction.Right right + diff --git a/src/Algebra/Action/Construct/Self.agda b/src/Algebra/Action/Construct/Self.agda new file mode 100644 index 0000000000..adecc31910 --- /dev/null +++ b/src/Algebra/Action/Construct/Self.agda @@ -0,0 +1,40 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Left- and right- regular actions +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Algebra.Action.Construct.Self where + +open import Algebra.Action.Bundles +open import Algebra.Action.Structures using (IsLeftAction; IsRightAction) +open import Algebra.Bundles using (Monoid) + +------------------------------------------------------------------------ +-- Left- and Right- Actions of a Monoid over itself + +module Regular {c ℓ} (M : Monoid c ℓ) where + + open Monoid M + open MonoidAction M setoid + + isLeftAction : IsLeftAction _≈_ _≈_ + isLeftAction = record { _▷_ = _∙_ ; ▷-cong = ∙-cong } + + isRightAction : IsRightAction _≈_ _≈_ + isRightAction = record { _◁_ = _∙_ ; ◁-cong = ∙-cong } + + leftAction : Left record { isLeftAction = isLeftAction } + leftAction = record + { ∙-act = assoc + ; ε-act = identityˡ + } + + rightAction : Right record { isRightAction = isRightAction } + rightAction = record + { ∙-act = λ x m n → sym (assoc x m n) + ; ε-act = identityʳ + } + diff --git a/src/Algebra/Action/Definitions.agda b/src/Algebra/Action/Definitions.agda new file mode 100644 index 0000000000..a66b3884e3 --- /dev/null +++ b/src/Algebra/Action/Definitions.agda @@ -0,0 +1,51 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Structure of the Action of one (pre-)Setoid on another +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_) + +module Algebra.Action.Definitions + {c a ℓ r} {M : Set c} {A : Set a} (_≈ᴹ_ : Rel M ℓ) (_≈_ : Rel A r) + where + +open import Algebra.Core using (Op₂) +open import Function.Base using (id) +open import Level using (Level; _⊔_) + +private + variable + x y : A + m n : M + + + +------------------------------------------------------------------------ +-- Basic definitions: fix notation + +Actˡ : Set (c ⊔ a) +Actˡ = M → A → A + +Actʳ : Set (c ⊔ a) +Actʳ = A → M → A + +Congruentˡ : Actˡ → Set (c ⊔ a ⊔ ℓ ⊔ r) +Congruentˡ _▷_ = _▷_ Preserves₂ _≈ᴹ_ ⟶ _≈_ ⟶ _≈_ + +Congruentʳ : Actʳ → Set (c ⊔ a ⊔ ℓ ⊔ r) +Congruentʳ _◁_ = _◁_ Preserves₂ _≈_ ⟶ _≈ᴹ_ ⟶ _≈_ + +IsActionˡ : Actˡ → Op₂ M → Set (c ⊔ a ⊔ r) +IsActionˡ _▷_ _∙_ = ∀ m n x → ((m ∙ n) ▷ x) ≈ (m ▷ (n ▷ x)) + +IsIdentityˡ : Actˡ → M → Set (a ⊔ r) +IsIdentityˡ _▷_ ε = ∀ x → (ε ▷ x) ≈ x + +IsActionʳ : Actʳ → Op₂ M → Set (c ⊔ a ⊔ r) +IsActionʳ _◁_ _∙_ = ∀ x m n → (x ◁ (m ∙ n)) ≈ ((x ◁ m) ◁ n) + +IsIdentityʳ : Actʳ → M → Set (a ⊔ r) +IsIdentityʳ _◁_ ε = ∀ x → (x ◁ ε) ≈ x diff --git a/src/Algebra/Action/Structures.agda b/src/Algebra/Action/Structures.agda new file mode 100644 index 0000000000..fec379bc25 --- /dev/null +++ b/src/Algebra/Action/Structures.agda @@ -0,0 +1,95 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Structure of the Action of one (pre-)Setoid on another +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Relation.Binary.Core using (Rel) + +module Algebra.Action.Structures + {c a ℓ r} {M : Set c} {A : Set a} (_≈ᴹ_ : Rel M ℓ) (_≈_ : Rel A r) + where + +open import Data.List.Base + using (List; []; _∷_; _++_; foldl; foldr) +open import Data.List.NonEmpty.Base + using (List⁺; _∷_) +open import Data.List.Relation.Binary.Pointwise as Pointwise + using (Pointwise; []; _∷_) +open import Function.Base using (id) +open import Level using (Level; _⊔_) + +open import Algebra.Action.Definitions _≈ᴹ_ _≈_ + +private + variable + x y z : A + m n p : M + ms ns ps : List M + + +------------------------------------------------------------------------ +-- Basic definitions: fix notation + +record IsLeftAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where + infixr 5 _▷_ _▷⋆_ _▷⁺_ + + field + _▷_ : Actˡ + ▷-cong : Congruentˡ _▷_ + +-- derived form: iterated action, satisfying congruence + + _▷⋆_ : List M → A → A + ms ▷⋆ a = foldr _▷_ a ms + + _▷⁺_ : List⁺ M → A → A + (m ∷ ms) ▷⁺ a = m ▷ ms ▷⋆ a + + ▷⋆-cong : Pointwise _≈ᴹ_ ms ns → x ≈ y → (ms ▷⋆ x) ≈ (ns ▷⋆ y) + ▷⋆-cong [] x≈y = x≈y + ▷⋆-cong (m≈n ∷ ms≋ns) x≈y = ▷-cong m≈n (▷⋆-cong ms≋ns x≈y) + + ▷⁺-cong : m ≈ᴹ n → Pointwise _≈ᴹ_ ms ns → x ≈ y → ((m ∷ ms) ▷⁺ x) ≈ ((n ∷ ns) ▷⁺ y) + ▷⁺-cong m≈n ms≋ns x≈y = ▷-cong m≈n (▷⋆-cong ms≋ns x≈y) + + ++-act-cong : ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) → + x ≈ y → (ps ▷⋆ x) ≈ (ms ▷⋆ ns ▷⋆ y) + ++-act-cong [] ps≋ns x≈y = ▷⋆-cong ps≋ns x≈y + ++-act-cong (m ∷ ms) (p≈m ∷ ps≋ms++ns) x≈y = ▷-cong p≈m (++-act-cong ms ps≋ms++ns x≈y) + + []-act-cong : x ≈ y → ([] ▷⋆ x) ≈ y + []-act-cong = id + + +record IsRightAction : Set (a ⊔ r ⊔ c ⊔ ℓ) where + infixl 5 _◁_ _◁⋆_ _◁⁺_ + + field + _◁_ : Actʳ + ◁-cong : Congruentʳ _◁_ + +-- derived form: iterated action, satisfying congruence + + _◁⋆_ : A → List M → A + a ◁⋆ ms = foldl _◁_ a ms + + _◁⁺_ : A → List⁺ M → A + a ◁⁺ (m ∷ ms) = a ◁ m ◁⋆ ms + + ◁⋆-cong : x ≈ y → Pointwise _≈ᴹ_ ms ns → (x ◁⋆ ms) ≈ (y ◁⋆ ns) + ◁⋆-cong x≈y [] = x≈y + ◁⋆-cong x≈y (m≈n ∷ ms≋ns) = ◁⋆-cong (◁-cong x≈y m≈n) ms≋ns + + ◁⁺-cong : x ≈ y → m ≈ᴹ n → Pointwise _≈ᴹ_ ms ns → (x ◁⁺ (m ∷ ms)) ≈ (y ◁⁺ (n ∷ ns)) + ◁⁺-cong x≈y m≈n ms≋ns = ◁⋆-cong (◁-cong x≈y m≈n) (ms≋ns) + + ++-act-cong : x ≈ y → ∀ ms → Pointwise _≈ᴹ_ ps (ms ++ ns) → + (x ◁⋆ ps) ≈ (y ◁⋆ ms ◁⋆ ns) + ++-act-cong x≈y [] ps≋ns = ◁⋆-cong x≈y ps≋ns + ++-act-cong x≈y (m ∷ ms) (p≈m ∷ ps≋ms++ns) = ++-act-cong (◁-cong x≈y p≈m) ms ps≋ms++ns + + []-act-cong : x ≈ y → (x ◁⋆ []) ≈ y + []-act-cong = id