diff --git a/master/Algebra.Definitions.RawMagma.html b/master/Algebra.Definitions.RawMagma.html index 9b8d0947bf..d19b6152d7 100644 --- a/master/Algebra.Definitions.RawMagma.html +++ b/master/Algebra.Definitions.RawMagma.html @@ -12,77 +12,98 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra.Bundles.Raw using (RawMagma) -open import Data.Product.Base using (_×_; ∃) -open import Level using (_⊔_) -open import Relation.Binary.Core using (Rel) -open import Relation.Nullary.Negation.Core using (¬_) +open import Data.Product.Base using (_×_) +open import Level using (_⊔_) +open import Relation.Binary.Core using (Rel) +open import Relation.Nullary.Negation.Core using (¬_) -module Algebra.Definitions.RawMagma - {a ℓ} (M : RawMagma a ℓ) - where +module Algebra.Definitions.RawMagma + {a ℓ} (M : RawMagma a ℓ) + where -open RawMagma M renaming (Carrier to A) +open RawMagma M renaming (Carrier to A) ------------------------------------------------------------------------- --- Divisibility +------------------------------------------------------------------------ +-- Divisibility -infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_ _∣∣_ _∤∤_ +infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_ _∥_ _∦_ --- Divisibility from the left. --- --- This and, the definition of right divisibility below, are defined as --- records rather than in terms of the base product type in order to --- make the use of pattern synonyms more ergonomic (see #2216 for --- further details). The record field names are not designed to be --- used explicitly and indeed aren't re-exported publicly by --- `Algebra.X.Properties.Divisibility` modules. +-- Divisibility from the left. +-- +-- This and, the definition of right divisibility below, are defined as +-- records rather than in terms of the base product type in order to +-- make the use of pattern synonyms more ergonomic (see #2216 for +-- further details). The record field names are not designed to be +-- used explicitly and indeed aren't re-exported publicly by +-- `Algebra.Properties.X.Divisibility` modules. -record _∣ˡ_ (x y : A) : Set (a ⊔ ℓ) where - constructor _,_ - field - quotient : A - equality : x ∙ quotient ≈ y +record _∣ˡ_ (x y : A) : Set (a ⊔ ℓ) where + constructor _,_ + field + quotient : A + equality : x ∙ quotient ≈ y -_∤ˡ_ : Rel A (a ⊔ ℓ) -x ∤ˡ y = ¬ x ∣ˡ y +_∤ˡ_ : Rel A (a ⊔ ℓ) +x ∤ˡ y = ¬ x ∣ˡ y --- Divisibility from the right +-- Divisibility from the right -record _∣ʳ_ (x y : A) : Set (a ⊔ ℓ) where - constructor _,_ - field - quotient : A - equality : quotient ∙ x ≈ y +record _∣ʳ_ (x y : A) : Set (a ⊔ ℓ) where + constructor _,_ + field + quotient : A + equality : quotient ∙ x ≈ y -_∤ʳ_ : Rel A (a ⊔ ℓ) -x ∤ʳ y = ¬ x ∣ʳ y +_∤ʳ_ : Rel A (a ⊔ ℓ) +x ∤ʳ y = ¬ x ∣ʳ y --- General divisibility +-- General divisibility --- The relations _∣ˡ_ and _∣ʳ_ are only equivalent when _∙_ is --- commutative. When that is not the case we take `_∣ʳ_` to be the --- primary one. +-- The relations _∣ˡ_ and _∣ʳ_ are only equivalent when _∙_ is +-- commutative. When that is not the case we take `_∣ʳ_` to be the +-- primary one. -_∣_ : Rel A (a ⊔ ℓ) -_∣_ = _∣ʳ_ +_∣_ : Rel A (a ⊔ ℓ) +_∣_ = _∣ʳ_ -_∤_ : Rel A (a ⊔ ℓ) -x ∤ y = ¬ x ∣ y +_∤_ : Rel A (a ⊔ ℓ) +x ∤ y = ¬ x ∣ y ------------------------------------------------------------------------- --- Mutual divisibility. +------------------------------------------------------------------------ +-- Mutual divisibility. --- In a monoid, this is an equivalence relation extending _≈_. --- When in a cancellative monoid, elements related by _∣∣_ are called --- associated, and `x ∣∣ y` means that `x` and `y` differ by some --- invertible factor. +-- In a monoid, this is an equivalence relation extending _≈_. +-- When in a cancellative monoid, elements related by _∣∣_ are called +-- associated, and `x ∣∣ y` means that `x` and `y` differ by some +-- invertible factor. --- Example: for ℕ this is equivalent to x ≡ y, --- for ℤ this is equivalent to (x ≡ y or x ≡ - y). +-- Example: for ℕ this is equivalent to x ≡ y, +-- for ℤ this is equivalent to (x ≡ y or x ≡ - y). -_∣∣_ : Rel A (a ⊔ ℓ) -x ∣∣ y = x ∣ y × y ∣ x +_∥_ : Rel A (a ⊔ ℓ) +x ∥ y = x ∣ y × y ∣ x + +_∦_ : Rel A (a ⊔ ℓ) +x ∦ y = ¬ x ∥ y + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.3 + +_∣∣_ = _∥_ +{-# WARNING_ON_USAGE _∣∣_ +"Warning: _∣∣_ was deprecated in v2.3. +Please use _∥_ instead." +#-} +_∤∤_ = _∦_ +{-# WARNING_ON_USAGE _∤∤_ +"Warning: _∤∤_ was deprecated in v2.3. +Please use _∦_ instead." +#-} -_∤∤_ : Rel A (a ⊔ ℓ) -x ∤∤ y = ¬ x ∣∣ y \ No newline at end of file diff --git a/master/Algebra.Definitions.RawSemiring.html b/master/Algebra.Definitions.RawSemiring.html index a37939a852..b2434a8a28 100644 --- a/master/Algebra.Definitions.RawSemiring.html +++ b/master/Algebra.Definitions.RawSemiring.html @@ -32,8 +32,8 @@ open import Algebra.Definitions.RawMonoid *-rawMonoid as Mult public using - ( _∣_ - ; _∤_ + ( _∣_ + ; _∤_ ) renaming ( sum to product @@ -70,18 +70,18 @@ -- Primality Coprime : Rel A (a ⊔ ℓ) -Coprime x y = ∀ {z} → z ∣ x → z ∣ y → z ∣ 1# +Coprime x y = ∀ {z} → z ∣ x → z ∣ y → z ∣ 1# record Irreducible (p : A) : Set (a ⊔ ℓ) where constructor mkIrred field - p∤1 : p ∤ 1# - split-∣1 : ∀ {x y} → p ≈ (x * y) → x ∣ 1# ⊎ y ∣ 1# + p∤1 : p ∤ 1# + split-∣1 : ∀ {x y} → p ≈ (x * y) → x ∣ 1# ⊎ y ∣ 1# record Prime (p : A) : Set (a ⊔ ℓ) where constructor mkPrime field p≉0 : p ≉ 0# - p∤1 : p ∤ 1# - split-∣ : ∀ {x y} → p ∣ x * y → p ∣ x ⊎ p ∣ y + p∤1 : p ∤ 1# + split-∣ : ∀ {x y} → p ∣ x * y → p ∣ x ⊎ p ∣ y \ No newline at end of file diff --git a/master/Algebra.Properties.CommutativeMagma.Divisibility.html b/master/Algebra.Properties.CommutativeMagma.Divisibility.html index fc1ea518c0..707e78dbb9 100644 --- a/master/Algebra.Properties.CommutativeMagma.Divisibility.html +++ b/master/Algebra.Properties.CommutativeMagma.Divisibility.html @@ -25,17 +25,17 @@ ------------------------------------------------------------------------ -- Further properties -x∣xy : ∀ x y → x ∣ x ∙ y -x∣xy x y = y , comm y x +x∣xy : ∀ x y → x ∣ x ∙ y +x∣xy x y = y , comm y x -xy≈z⇒x∣z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z -xy≈z⇒x∣z x y xy≈z = ∣-respʳ xy≈z (x∣xy x y) +xy≈z⇒x∣z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z +xy≈z⇒x∣z x y xy≈z = ∣-respʳ xy≈z (x∣xy x y) -x|xy∧y|xy : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y) -x|xy∧y|xy x y = x∣xy x y , x∣yx y x +x|xy∧y|xy : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y) +x|xy∧y|xy x y = x∣xy x y , x∣yx y x -xy≈z⇒x|z∧y|z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z × y ∣ z -xy≈z⇒x|z∧y|z x y xy≈z = xy≈z⇒x∣z x y xy≈z , xy≈z⇒y∣z x y xy≈z +xy≈z⇒x|z∧y|z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z × y ∣ z +xy≈z⇒x|z∧y|z x y xy≈z = xy≈z⇒x∣z x y xy≈z , xy≈z⇒y∣z x y xy≈z ------------------------------------------------------------------------ diff --git a/master/Algebra.Properties.CommutativeSemigroup.Divisibility.html b/master/Algebra.Properties.CommutativeSemigroup.Divisibility.html index 76aa025525..fc5997691d 100644 --- a/master/Algebra.Properties.CommutativeSemigroup.Divisibility.html +++ b/master/Algebra.Properties.CommutativeSemigroup.Divisibility.html @@ -33,15 +33,15 @@ ------------------------------------------------------------------------ -- New properties -x∣y∧z∣x/y⇒xz∣y : ∀ {x y z} → ((x/y , _) : x ∣ y) → z ∣ x/y → x ∙ z ∣ y -x∣y∧z∣x/y⇒xz∣y {x} {y} {z} (x/y , x/y∙x≈y) (p , pz≈x/y) = p , (begin +x∣y∧z∣x/y⇒xz∣y : ∀ {x y z} → ((x/y , _) : x ∣ y) → z ∣ x/y → x ∙ z ∣ y +x∣y∧z∣x/y⇒xz∣y {x} {y} {z} (x/y , x/y∙x≈y) (p , pz≈x/y) = p , (begin p ∙ (x ∙ z) ≈⟨ x∙yz≈xz∙y p x z ⟩ (p ∙ z) ∙ x ≈⟨ ∙-congʳ pz≈x/y ⟩ x/y ∙ x ≈⟨ x/y∙x≈y ⟩ y ∎) -x∣y⇒zx∣zy : ∀ {x y} z → x ∣ y → z ∙ x ∣ z ∙ y -x∣y⇒zx∣zy {x} {y} z (q , qx≈y) = q , (begin +x∣y⇒zx∣zy : ∀ {x y} z → x ∣ y → z ∙ x ∣ z ∙ y +x∣y⇒zx∣zy {x} {y} z (q , qx≈y) = q , (begin q ∙ (z ∙ x) ≈⟨ x∙yz≈y∙xz q z x ⟩ z ∙ (q ∙ x) ≈⟨ ∙-congˡ qx≈y ⟩ z ∙ y ∎) diff --git a/master/Algebra.Properties.Magma.Divisibility.html b/master/Algebra.Properties.Magma.Divisibility.html index b0396ac9f9..06edf0fb25 100644 --- a/master/Algebra.Properties.Magma.Divisibility.html +++ b/master/Algebra.Properties.Magma.Divisibility.html @@ -22,90 +22,133 @@ -- Re-export divisibility relations publicly open import Algebra.Definitions.RawMagma rawMagma public - using (_∣_; _∤_; _∣∣_; _∤∤_; _∣ˡ_; _∤ˡ_; _∣ʳ_; _∤ʳ_; _,_) + using (_∣_; _∤_; _∥_; _∦_; _∣ˡ_; _∤ˡ_; _∣ʳ_; _∤ʳ_; _,_) ------------------------------------------------------------------------- --- Properties of divisibility +------------------------------------------------------------------------ +-- Properties of divisibility -∣-respʳ-≈ : _∣_ Respectsʳ _≈_ -∣-respʳ-≈ y≈z (q , qx≈y) = q , trans qx≈y y≈z +∣-respʳ-≈ : _∣_ Respectsʳ _≈_ +∣-respʳ-≈ y≈z (q , qx≈y) = q , trans qx≈y y≈z -∣-respˡ-≈ : _∣_ Respectsˡ _≈_ -∣-respˡ-≈ x≈z (q , qx≈y) = q , trans (∙-congˡ (sym x≈z)) qx≈y +∣-respˡ-≈ : _∣_ Respectsˡ _≈_ +∣-respˡ-≈ x≈z (q , qx≈y) = q , trans (∙-congˡ (sym x≈z)) qx≈y -∣-resp-≈ : _∣_ Respects₂ _≈_ -∣-resp-≈ = ∣-respʳ-≈ , ∣-respˡ-≈ +∣-resp-≈ : _∣_ Respects₂ _≈_ +∣-resp-≈ = ∣-respʳ-≈ , ∣-respˡ-≈ -x∣yx : ∀ x y → x ∣ y ∙ x -x∣yx x y = y , refl +x∣yx : ∀ x y → x ∣ y ∙ x +x∣yx x y = y , refl -xy≈z⇒y∣z : ∀ x y {z} → x ∙ y ≈ z → y ∣ z -xy≈z⇒y∣z x y xy≈z = ∣-respʳ-≈ xy≈z (x∣yx y x) +xy≈z⇒y∣z : ∀ x y {z} → x ∙ y ≈ z → y ∣ z +xy≈z⇒y∣z x y xy≈z = ∣-respʳ-≈ xy≈z (x∣yx y x) ------------------------------------------------------------------------- --- Properties of non-divisibility +------------------------------------------------------------------------ +-- Properties of non-divisibility -∤-respˡ-≈ : _∤_ Respectsˡ _≈_ -∤-respˡ-≈ x≈y x∤z y∣z = contradiction (∣-respˡ-≈ (sym x≈y) y∣z) x∤z +∤-respˡ-≈ : _∤_ Respectsˡ _≈_ +∤-respˡ-≈ x≈y x∤z y∣z = contradiction (∣-respˡ-≈ (sym x≈y) y∣z) x∤z -∤-respʳ-≈ : _∤_ Respectsʳ _≈_ -∤-respʳ-≈ x≈y z∤x z∣y = contradiction (∣-respʳ-≈ (sym x≈y) z∣y) z∤x +∤-respʳ-≈ : _∤_ Respectsʳ _≈_ +∤-respʳ-≈ x≈y z∤x z∣y = contradiction (∣-respʳ-≈ (sym x≈y) z∣y) z∤x -∤-resp-≈ : _∤_ Respects₂ _≈_ -∤-resp-≈ = ∤-respʳ-≈ , ∤-respˡ-≈ +∤-resp-≈ : _∤_ Respects₂ _≈_ +∤-resp-≈ = ∤-respʳ-≈ , ∤-respˡ-≈ ------------------------------------------------------------------------- --- Properties of mutual divisibility _∣∣_ +------------------------------------------------------------------------ +-- Properties of mutual divisibility _∥_ -∣∣-sym : Symmetric _∣∣_ -∣∣-sym = swap +∥-sym : Symmetric _∥_ +∥-sym = swap -∣∣-respˡ-≈ : _∣∣_ Respectsˡ _≈_ -∣∣-respˡ-≈ x≈z (x∣y , y∣x) = ∣-respˡ-≈ x≈z x∣y , ∣-respʳ-≈ x≈z y∣x +∥-respˡ-≈ : _∥_ Respectsˡ _≈_ +∥-respˡ-≈ x≈z (x∣y , y∣x) = ∣-respˡ-≈ x≈z x∣y , ∣-respʳ-≈ x≈z y∣x -∣∣-respʳ-≈ : _∣∣_ Respectsʳ _≈_ -∣∣-respʳ-≈ y≈z (x∣y , y∣x) = ∣-respʳ-≈ y≈z x∣y , ∣-respˡ-≈ y≈z y∣x +∥-respʳ-≈ : _∥_ Respectsʳ _≈_ +∥-respʳ-≈ y≈z (x∣y , y∣x) = ∣-respʳ-≈ y≈z x∣y , ∣-respˡ-≈ y≈z y∣x -∣∣-resp-≈ : _∣∣_ Respects₂ _≈_ -∣∣-resp-≈ = ∣∣-respʳ-≈ , ∣∣-respˡ-≈ +∥-resp-≈ : _∥_ Respects₂ _≈_ +∥-resp-≈ = ∥-respʳ-≈ , ∥-respˡ-≈ ------------------------------------------------------------------------- --- Properties of mutual non-divisibility _∤∤_ +------------------------------------------------------------------------ +-- Properties of mutual non-divisibility _∤∤_ -∤∤-sym : Symmetric _∤∤_ -∤∤-sym x∤∤y y∣∣x = contradiction (∣∣-sym y∣∣x) x∤∤y +∦-sym : Symmetric _∦_ +∦-sym x∦y y∥x = contradiction (∥-sym y∥x) x∦y -∤∤-respˡ-≈ : _∤∤_ Respectsˡ _≈_ -∤∤-respˡ-≈ x≈y x∤∤z y∣∣z = contradiction (∣∣-respˡ-≈ (sym x≈y) y∣∣z) x∤∤z +∦-respˡ-≈ : _∦_ Respectsˡ _≈_ +∦-respˡ-≈ x≈y x∦z y∥z = contradiction (∥-respˡ-≈ (sym x≈y) y∥z) x∦z -∤∤-respʳ-≈ : _∤∤_ Respectsʳ _≈_ -∤∤-respʳ-≈ x≈y z∤∤x z∣∣y = contradiction (∣∣-respʳ-≈ (sym x≈y) z∣∣y) z∤∤x +∦-respʳ-≈ : _∦_ Respectsʳ _≈_ +∦-respʳ-≈ x≈y z∦x z∥y = contradiction (∥-respʳ-≈ (sym x≈y) z∥y) z∦x -∤∤-resp-≈ : _∤∤_ Respects₂ _≈_ -∤∤-resp-≈ = ∤∤-respʳ-≈ , ∤∤-respˡ-≈ +∦-resp-≈ : _∦_ Respects₂ _≈_ +∦-resp-≈ = ∦-respʳ-≈ , ∦-respˡ-≈ ------------------------------------------------------------------------- --- DEPRECATED NAMES ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. --- Version 2.2 +-- Version 2.2 -∣-respˡ = ∣-respˡ-≈ -{-# WARNING_ON_USAGE ∣-respˡ -"Warning: ∣-respˡ was deprecated in v2.2. +∣-respˡ = ∣-respˡ-≈ +{-# WARNING_ON_USAGE ∣-respˡ +"Warning: ∣-respˡ was deprecated in v2.2. Please use ∣-respˡ-≈ instead. " -#-} -∣-respʳ = ∣-respʳ-≈ -{-# WARNING_ON_USAGE ∣-respʳ -"Warning: ∣-respʳ was deprecated in v2.2. +#-} +∣-respʳ = ∣-respʳ-≈ +{-# WARNING_ON_USAGE ∣-respʳ +"Warning: ∣-respʳ was deprecated in v2.2. Please use ∣-respʳ-≈ instead. " -#-} -∣-resp = ∣-resp-≈ -{-# WARNING_ON_USAGE ∣-resp -"Warning: ∣-resp was deprecated in v2.2. +#-} +∣-resp = ∣-resp-≈ +{-# WARNING_ON_USAGE ∣-resp +"Warning: ∣-resp was deprecated in v2.2. Please use ∣-resp-≈ instead. " -#-} +#-} + +-- Version 2.3 + +∣∣-sym = ∥-sym +{-# WARNING_ON_USAGE ∣∣-sym +"Warning: ∣∣-sym was deprecated in v2.3. +Please use ∥-sym instead. " +#-} +∣∣-respˡ-≈ = ∥-respˡ-≈ +{-# WARNING_ON_USAGE ∣∣-respˡ-≈ +"Warning: ∣∣-respˡ-≈ was deprecated in v2.3. +Please use ∥-respˡ-≈ instead. " +#-} +∣∣-respʳ-≈ = ∥-respʳ-≈ +{-# WARNING_ON_USAGE ∣∣-respʳ-≈ +"Warning: ∣∣-respʳ-≈ was deprecated in v2.3. +Please use ∥-respʳ-≈ instead. " +#-} +∣∣-resp-≈ = ∥-resp-≈ +{-# WARNING_ON_USAGE ∣∣-resp-≈ +"Warning: ∣∣-resp-≈ was deprecated in v2.3. +Please use ∥-resp-≈ instead. " +#-} +∤∤-sym = ∦-sym +{-# WARNING_ON_USAGE ∤∤-sym +"Warning: ∤∤-sym was deprecated in v2.3. +Please use ∦-sym instead. " +#-} +∤∤-respˡ-≈ = ∦-respˡ-≈ +{-# WARNING_ON_USAGE ∤∤-respˡ-≈ +"Warning: ∤∤-respˡ-≈ was deprecated in v2.3. +Please use ∦-respˡ-≈ instead. " +#-} +∤∤-respʳ-≈ = ∦-respʳ-≈ +{-# WARNING_ON_USAGE ∤∤-respʳ-≈ +"Warning: ∤∤-respʳ-≈ was deprecated in v2.3. +Please use ∦-respʳ-≈ instead. " +#-} +∤∤-resp-≈ = ∦-resp-≈ +{-# WARNING_ON_USAGE ∤∤-resp-≈ +"Warning: ∤∤-resp-≈ was deprecated in v2.3. +Please use ∦-resp-≈ instead. " +#-} \ No newline at end of file diff --git a/master/Algebra.Properties.Monoid.Divisibility.html b/master/Algebra.Properties.Monoid.Divisibility.html index 4f0a98902c..4f05496196 100644 --- a/master/Algebra.Properties.Monoid.Divisibility.html +++ b/master/Algebra.Properties.Monoid.Divisibility.html @@ -29,16 +29,16 @@ infix 4 ε∣_ -ε∣_ : ∀ x → ε ∣ x -ε∣ x = x , identityʳ x +ε∣_ : ∀ x → ε ∣ x +ε∣ x = x , identityʳ x -∣-refl : Reflexive _∣_ -∣-refl {x} = ε , identityˡ x +∣-refl : Reflexive _∣_ +∣-refl {x} = ε , identityˡ x -∣-reflexive : _≈_ ⇒ _∣_ -∣-reflexive x≈y = ε , trans (identityˡ _) x≈y +∣-reflexive : _≈_ ⇒ _∣_ +∣-reflexive x≈y = ε , trans (identityˡ _) x≈y -∣-isPreorder : IsPreorder _≈_ _∣_ +∣-isPreorder : IsPreorder _≈_ _∣_ ∣-isPreorder = record { isEquivalence = isEquivalence ; reflexive = ∣-reflexive @@ -53,16 +53,43 @@ ------------------------------------------------------------------------ -- Properties of mutual divisibiity -∣∣-refl : Reflexive _∣∣_ -∣∣-refl = ∣-refl , ∣-refl - -∣∣-reflexive : _≈_ ⇒ _∣∣_ -∣∣-reflexive x≈y = ∣-reflexive x≈y , ∣-reflexive (sym x≈y) - -∣∣-isEquivalence : IsEquivalence _∣∣_ -∣∣-isEquivalence = record - { refl = λ {x} → ∣∣-refl {x} - ; sym = λ {x} {y} → ∣∣-sym {x} {y} - ; trans = λ {x} {y} {z} → ∣∣-trans {x} {y} {z} - } +∥-refl : Reflexive _∥_ +∥-refl = ∣-refl , ∣-refl + +∥-reflexive : _≈_ ⇒ _∥_ +∥-reflexive x≈y = ∣-reflexive x≈y , ∣-reflexive (sym x≈y) + +∥-isEquivalence : IsEquivalence _∥_ +∥-isEquivalence = record + { refl = λ {x} → ∥-refl {x} + ; sym = λ {x} {y} → ∥-sym {x} {y} + ; trans = λ {x} {y} {z} → ∥-trans {x} {y} {z} + } + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.3 + +∣∣-refl = ∥-refl +{-# WARNING_ON_USAGE ∣∣-refl +"Warning: ∣∣-refl was deprecated in v2.3. +Please use ∥-refl instead. " +#-} + +∣∣-reflexive = ∥-reflexive +{-# WARNING_ON_USAGE ∣∣-reflexive +"Warning: ∣∣-reflexive was deprecated in v2.3. +Please use ∥-reflexive instead. " +#-} + +∣∣-isEquivalence = ∥-isEquivalence +{-# WARNING_ON_USAGE ∣∣-isEquivalence +"Warning: ∣∣-isEquivalence was deprecated in v2.3. +Please use ∥-isEquivalence instead. " +#-} \ No newline at end of file diff --git a/master/Algebra.Properties.Semigroup.Divisibility.html b/master/Algebra.Properties.Semigroup.Divisibility.html index 38edca82a9..be5ace7348 100644 --- a/master/Algebra.Properties.Semigroup.Divisibility.html +++ b/master/Algebra.Properties.Semigroup.Divisibility.html @@ -24,13 +24,28 @@ ------------------------------------------------------------------------ -- Properties of _∣_ -∣-trans : Transitive _∣_ -∣-trans (p , px≈y) (q , qy≈z) = - q ∙ p , trans (assoc q p _) (trans (∙-congˡ px≈y) qy≈z) +∣-trans : Transitive _∣_ +∣-trans (p , px≈y) (q , qy≈z) = + q ∙ p , trans (assoc q p _) (trans (∙-congˡ px≈y) qy≈z) ------------------------------------------------------------------------ --- Properties of _∣∣_ +-- Properties of _∥_ -∣∣-trans : Transitive _∣∣_ -∣∣-trans (x∣y , y∣x) (y∣z , z∣y) = ∣-trans x∣y y∣z , ∣-trans z∣y y∣x +∥-trans : Transitive _∥_ +∥-trans (x∣y , y∣x) (y∣z , z∣y) = ∣-trans x∣y y∣z , ∣-trans z∣y y∣x + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.3 + +∣∣-trans = ∥-trans +{-# WARNING_ON_USAGE ∣∣-trans +"Warning: ∣∣-trans was deprecated in v2.3. +Please use ∥-trans instead. " +#-} \ No newline at end of file diff --git a/master/Algebra.Properties.Semiring.Divisibility.html b/master/Algebra.Properties.Semiring.Divisibility.html index f97b4d3a87..065e9cd5cf 100644 --- a/master/Algebra.Properties.Semiring.Divisibility.html +++ b/master/Algebra.Properties.Semiring.Divisibility.html @@ -28,15 +28,15 @@ infixr 8 _∣0 -_∣0 : ∀ x → x ∣ 0# -x ∣0 = 0# , zeroˡ x +_∣0 : ∀ x → x ∣ 0# +x ∣0 = 0# , zeroˡ x -0∣x⇒x≈0 : ∀ {x} → 0# ∣ x → x ≈ 0# -0∣x⇒x≈0 (q , q*0≈x) = trans (sym q*0≈x) (zeroʳ q) +0∣x⇒x≈0 : ∀ {x} → 0# ∣ x → x ≈ 0# +0∣x⇒x≈0 (q , q*0≈x) = trans (sym q*0≈x) (zeroʳ q) -x∣y∧y≉0⇒x≉0 : ∀ {x y} → x ∣ y → y ≉ 0# → x ≉ 0# -x∣y∧y≉0⇒x≉0 x∣y y≉0 x≈0 = y≉0 (0∣x⇒x≈0 (∣-respˡ x≈0 x∣y)) +x∣y∧y≉0⇒x≉0 : ∀ {x y} → x ∣ y → y ≉ 0# → x ≉ 0# +x∣y∧y≉0⇒x≉0 x∣y y≉0 x≈0 = y≉0 (0∣x⇒x≈0 (∣-respˡ x≈0 x∣y)) -0∤1 : 0# ≉ 1# → 0# ∤ 1# -0∤1 0≉1 (q , q*0≈1) = 0≉1 (trans (sym (zeroʳ q)) q*0≈1) +0∤1 : 0# ≉ 1# → 0# ∤ 1# +0∤1 0≉1 (q , q*0≈1) = 0≉1 (trans (sym (zeroʳ q)) q*0≈1) \ No newline at end of file diff --git a/master/Algebra.Properties.Semiring.Primality.html b/master/Algebra.Properties.Semiring.Primality.html index 96c6eaa984..2cf0adc9f7 100644 --- a/master/Algebra.Properties.Semiring.Primality.html +++ b/master/Algebra.Properties.Semiring.Primality.html @@ -31,7 +31,7 @@ Coprime-sym : Symmetric Coprime Coprime-sym coprime = flip coprime -∣1⇒Coprime : ∀ {x} y → x ∣ 1# → Coprime x y +∣1⇒Coprime : ∀ {x} y → x ∣ 1# → Coprime x y ∣1⇒Coprime {x} y x∣1 z∣x _ = ∣-trans z∣x x∣1 ------------------------------------------------------------------------ diff --git a/master/Data.Nat.Base.html b/master/Data.Nat.Base.html index 8ae4593a09..e0d6997976 100644 --- a/master/Data.Nat.Base.html +++ b/master/Data.Nat.Base.html @@ -13,7 +13,7 @@ module Data.Nat.Base where open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring) -open import Algebra.Definitions.RawMagma using (_∣ˡ_; _,_) +open import Algebra.Definitions.RawMagma using (_∣ˡ_; _,_) open import Data.Bool.Base using (Bool; true; false; T; not) open import Data.Parity.Base using (Parity; 0ℙ; 1ℙ) open import Level using (0ℓ) @@ -364,7 +364,7 @@ infix 4 _≤″_ _<″_ _≥″_ _>″_ _≤″_ : (m n : ℕ) → Set -_≤″_ = _∣ˡ_ +-rawMagma +_≤″_ = _∣ˡ_ +-rawMagma _<″_ : Rel ℕ 0ℓ m <″ n = suc m ≤″ n @@ -378,7 +378,7 @@ -- Smart destructor of _<″_ s<″s⁻¹ : ∀ {m n} → suc m <″ suc n → m <″ n -s<″s⁻¹ (k , eq) = k , cong pred eq +s<″s⁻¹ (k , eq) = k , cong pred eq -- _≤‴_: this definition is useful for induction with an upper bound. @@ -445,7 +445,7 @@ -- Smart destructor of _≤″_ s≤″s⁻¹ : ∀ {m n} → suc m ≤″ suc n → m ≤″ n -s≤″s⁻¹ (k , eq) = k , cong pred eq +s≤″s⁻¹ (k , eq) = k , cong pred eq {-# WARNING_ON_USAGE s≤″s⁻¹ "Warning: s≤″s⁻¹ was deprecated in v2.1. Please match directly on proofs of ≤″ using constructor Algebra.Definitions.RawMagma._∣ˡ_._,_ instead. " #-} diff --git a/master/Data.Nat.Properties.html b/master/Data.Nat.Properties.html index 62e0a8a54d..ccca24dd28 100644 --- a/master/Data.Nat.Properties.html +++ b/master/Data.Nat.Properties.html @@ -15,7 +15,7 @@ open import Axiom.UniquenessOfIdentityProofs using (module Decidable⇒UIP) open import Algebra.Bundles using (Magma; Semigroup; CommutativeSemigroup; CommutativeMonoid; Monoid; Semiring; CommutativeSemiring; CommutativeSemiringWithoutOne) -open import Algebra.Definitions.RawMagma using (_,_) +open import Algebra.Definitions.RawMagma using (_,_) open import Algebra.Morphism open import Algebra.Consequences.Propositional using (comm+cancelˡ⇒cancelʳ; comm∧distrʳ⇒distrˡ; comm∧distrˡ⇒distrʳ) @@ -2120,18 +2120,18 @@ -- equivalence of _≤″_ to _≤_ ≤⇒≤″ : _≤_ ⇒ _≤″_ -≤⇒≤″ = (_ ,_) ∘ m+[n∸m]≡n +≤⇒≤″ = (_ ,_) ∘ m+[n∸m]≡n <⇒<″ : _<_ ⇒ _<″_ <⇒<″ = ≤⇒≤″ ≤″⇒≤ : _≤″_ ⇒ _≤_ -≤″⇒≤ (k , refl) = m≤m+n _ k +≤″⇒≤ (k , refl) = m≤m+n _ k -- equivalence to the old definition of _≤″_ ≤″-proof : (le : m ≤″ n) → let k , _ = le in m + k ≡ n -≤″-proof (_ , prf) = prf +≤″-proof (_ , prf) = prf -- yielding analogous proof for _≤_ @@ -2156,7 +2156,7 @@ <ᵇ⇒<″ {m} {n} = <⇒<″ ∘ (<ᵇ⇒< m n) <″⇒<ᵇ : ∀ {m n} → m <″ n → T (m <ᵇ n) -<″⇒<ᵇ {m} (k , refl) = <⇒<ᵇ (m≤m+n (suc m) k) +<″⇒<ᵇ {m} (k , refl) = <⇒<ᵇ (m≤m+n (suc m) k) -- NB: we use the builtin function `_<ᵇ_ : (m n : ℕ) → Bool` here so -- that the function quickly decides whether to return `yes` or `no`. @@ -2170,7 +2170,7 @@ m <″? n = map′ <ᵇ⇒<″ <″⇒<ᵇ (T? (m <ᵇ n)) _≤″?_ : Decidable _≤″_ -zero ≤″? n = yes (n , refl) +zero ≤″? n = yes (n , refl) suc m ≤″? n = m <″? n _≥″?_ : Decidable _≥″_ @@ -2180,9 +2180,9 @@ _>″?_ = flip _<″?_ ≤″-irrelevant : Irrelevant _≤″_ -≤″-irrelevant {m} (_ , eq₁) (_ , eq₂) +≤″-irrelevant {m} (_ , eq₁) (_ , eq₂) with refl ← +-cancelˡ-≡ m _ _ (trans eq₁ (sym eq₂)) - = cong (_ ,_) (≡-irrelevant eq₁ eq₂) + = cong (_ ,_) (≡-irrelevant eq₁ eq₂) <″-irrelevant : Irrelevant _<″_ <″-irrelevant = ≤″-irrelevant @@ -2198,8 +2198,8 @@ ------------------------------------------------------------------------ ≤‴⇒≤″ : m ≤‴ n → m ≤″ n -≤‴⇒≤″ ≤‴-refl = _ , +-identityʳ _ -≤‴⇒≤″ (≤‴-step m≤n) = _ , trans (+-suc _ _) (≤″-proof (≤‴⇒≤″ m≤n)) +≤‴⇒≤″ ≤‴-refl = _ , +-identityʳ _ +≤‴⇒≤″ (≤‴-step m≤n) = _ , trans (+-suc _ _) (≤″-proof (≤‴⇒≤″ m≤n)) m≤‴m+k : m + k ≡ n → m ≤‴ n m≤‴m+k {k = zero} = ≤‴-reflexive ∘ trans (sym (+-identityʳ _)) diff --git a/master/Data.Nat.WithK.html b/master/Data.Nat.WithK.html index b6e8cdef84..93f5e51c0d 100644 --- a/master/Data.Nat.WithK.html +++ b/master/Data.Nat.WithK.html @@ -9,10 +9,10 @@ module Data.Nat.WithK where -open import Algebra.Definitions.RawMagma using (_,_) +open import Algebra.Definitions.RawMagma using (_,_) open import Data.Nat.Base open import Relation.Binary.PropositionalEquality.WithK ≤″-erase : ∀ {m n} → m ≤″ n → m ≤″ n -≤″-erase (_ , eq) = _ , ≡-erase eq +≤″-erase (_ , eq) = _ , ≡-erase eq \ No newline at end of file