------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of left-scaling
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Core
using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
-- The properties are parameterised by the two carriers and
-- the result equality.
module Algebra.Module.Definitions.Left
{a b ℓb} (A : Set a) {B : Set b} (_≈_ : Rel B ℓb)
where
------------------------------------------------------------------------
-- Binary operations
open import Algebra.Core using (Op₂)
open import Algebra.Module.Core using (Opₗ)
------------------------------------------------------------------------
-- Properties of operations
LeftIdentity : A → Opₗ A B → Set _
LeftIdentity a _∙ᴮ_ = ∀ m → (a ∙ᴮ m) ≈ m
Associative : Op₂ A → Opₗ A B → Set _
Associative _∙ᴬ_ _∙ᴮ_ = ∀ x y m → ((x ∙ᴬ y) ∙ᴮ m) ≈ (x ∙ᴮ (y ∙ᴮ m))
infix 4 _DistributesOverˡ_ _DistributesOverʳ_⟶_
_DistributesOverˡ_ : Opₗ A B → Op₂ B → Set _
_*_ DistributesOverˡ _+_ =
∀ x m n → (x * (m + n)) ≈ ((x * m) + (x * n))
_DistributesOverʳ_⟶_ : Opₗ A B → Op₂ A → Op₂ B → Set _
_*_ DistributesOverʳ _+ᴬ_ ⟶ _+ᴮ_ =
∀ x m n → ((m +ᴬ n) * x) ≈ ((m * x) +ᴮ (n * x))
LeftZero : A → B → Opₗ A B → Set _
LeftZero zᴬ zᴮ _∙_ = ∀ x → (zᴬ ∙ x) ≈ zᴮ
RightZero : B → Opₗ A B → Set _
RightZero z _∙_ = ∀ x → (x ∙ z) ≈ z
Commutative : Opₗ A B → Set _
Commutative _∙_ = ∀ x y m → (x ∙ (y ∙ m)) ≈ (y ∙ (x ∙ m))
LeftCongruent : Opₗ A B → Set _
LeftCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_
RightCongruent : ∀ {ℓa} → Rel A ℓa → Opₗ A B → Set _
RightCongruent ≈ᴬ _∙_ = ∀ {m} → (_∙ m) Preserves ≈ᴬ ⟶ _≈_
Congruent : ∀ {ℓa} → Rel A ℓa → Opₗ A B → Set _
Congruent ≈ᴬ ∙ = ∙ Preserves₂ ≈ᴬ ⟶ _≈_ ⟶ _≈_
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4