[ refactor ] name of Data.Product.Relation.Binary.Pointwise.NonDependent.×-decidable

CHANGELOG.md

@@ -89,6 +89,13 @@ Deprecated names
   ¬∀⟶∃¬-          ↦   ¬∀⇒∃¬
   ```
 
+* In `Data.Product.Relation.Binary.Pointwise.NonDependent`:
+  ```agda
+  Pointwise      ↦  _×_
+  ×-decidable    ↦  _×?_
+  Pointwise-≡↔≡  ↦  ×-≡↔≡-×
+  ```
+
 * In `Data.Rational.Properties`:
   ```agda
   nonPos*nonPos⇒nonPos  ↦  nonPos*nonPos⇒nonNeg

src/Algebra/Construct/DirectProduct.agda

@@ -16,7 +16,7 @@
 module Algebra.Construct.DirectProduct where
 
 open import Algebra
-open import Data.Product.Base using (_×_; zip; _,_; map; _<*>_; uncurry)
+open import Data.Product.Base as Product using (zip; _,_; map; _<*>_; uncurry)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Level using (Level; _⊔_)
 
@@ -29,32 +29,32 @@ private
 
 rawMagma : RawMagma a ℓ₁ → RawMagma b ℓ₂ → RawMagma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 rawMagma M N = record
-  { Carrier = M.Carrier × N.Carrier
-  ; _≈_     = Pointwise M._≈_ N._≈_
+  { Carrier = M.Carrier Product.× N.Carrier
+  ; _≈_     = M._≈_ × N._≈_
   ; _∙_     = zip M._∙_ N._∙_
   } where module M = RawMagma M; module N = RawMagma N
 
 rawMonoid : RawMonoid a ℓ₁ → RawMonoid b ℓ₂ → RawMonoid (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 rawMonoid M N = record
-  { Carrier = M.Carrier × N.Carrier
-  ; _≈_     = Pointwise M._≈_ N._≈_
+  { Carrier = M.Carrier Product.× N.Carrier
+  ; _≈_     = M._≈_ × N._≈_
   ; _∙_     = zip M._∙_ N._∙_
   ; ε       = M.ε , N.ε
   } where module M = RawMonoid M; module N = RawMonoid N
 
 rawGroup : RawGroup a ℓ₁ → RawGroup b ℓ₂ → RawGroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 rawGroup G H = record
-  { Carrier = G.Carrier × H.Carrier
-  ; _≈_     = Pointwise G._≈_ H._≈_
+  { Carrier = G.Carrier Product.× H.Carrier
+  ; _≈_     = G._≈_ × H._≈_
   ; _∙_     = zip G._∙_ H._∙_
   ; ε       = G.ε , H.ε
   ; _⁻¹     = map G._⁻¹ H._⁻¹
   } where module G = RawGroup G; module H = RawGroup H
 
 rawSemiring : RawSemiring a ℓ₁ → RawSemiring b ℓ₂ → RawSemiring (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 rawSemiring R S = record
-  { Carrier = R.Carrier × S.Carrier
-  ; _≈_     = Pointwise R._≈_ S._≈_
+  { Carrier = R.Carrier Product.× S.Carrier
+  ; _≈_     = R._≈_ × S._≈_
   ; _+_     = zip R._+_ S._+_
   ; _*_     = zip R._*_ S._*_
   ; 0#      = R.0# , S.0#
@@ -63,8 +63,8 @@ rawSemiring R S = record
 
 rawRingWithoutOne : RawRingWithoutOne a ℓ₁ → RawRingWithoutOne b ℓ₂ → RawRingWithoutOne (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 rawRingWithoutOne R S = record
-  { Carrier = R.Carrier × S.Carrier
-  ; _≈_     = Pointwise R._≈_ S._≈_
+  { Carrier = R.Carrier Product.× S.Carrier
+  ; _≈_     = R._≈_ × S._≈_
   ; _+_     = zip R._+_ S._+_
   ; _*_     = zip R._*_ S._*_
   ; -_      = map R.-_ S.-_
@@ -73,8 +73,8 @@ rawRingWithoutOne R S = record
 
 rawRing : RawRing a ℓ₁ → RawRing b ℓ₂ → RawRing (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 rawRing R S = record
-  { Carrier = R.Carrier × S.Carrier
-  ; _≈_     = Pointwise R._≈_ S._≈_
+  { Carrier = R.Carrier Product.× S.Carrier
+  ; _≈_     = R._≈_ × S._≈_
   ; _+_     = zip R._+_ S._+_
   ; _*_     = zip R._*_ S._*_
   ; -_      = map R.-_ S.-_
@@ -84,17 +84,17 @@ rawRing R S = record
 
 rawQuasigroup : RawQuasigroup a ℓ₁ → RawQuasigroup b ℓ₂ → RawQuasigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 rawQuasigroup M N = record
-  { Carrier = M.Carrier × N.Carrier
-  ; _≈_     = Pointwise M._≈_ N._≈_
+  { Carrier = M.Carrier Product.× N.Carrier
+  ; _≈_     = M._≈_ × N._≈_
   ; _∙_     = zip M._∙_ N._∙_
   ; _\\_    = zip M._\\_ N._\\_
   ; _//_    = zip M._//_ N._//_
   } where module M = RawQuasigroup M; module N = RawQuasigroup N
 
 rawLoop : RawLoop a ℓ₁ → RawLoop b ℓ₂ → RawLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 rawLoop M N = record
-  { Carrier = M.Carrier × N.Carrier
-  ; _≈_     = Pointwise M._≈_ N._≈_
+  { Carrier = M.Carrier Product.× N.Carrier
+  ; _≈_     = M._≈_ × N._≈_
   ; _∙_     = zip M._∙_ N._∙_
   ; _\\_    = zip M._\\_ N._\\_
   ; _//_    = zip M._//_ N._//_
@@ -106,8 +106,8 @@ rawLoop M N = record
 
 magma : Magma a ℓ₁ → Magma b ℓ₂ → Magma (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
 magma M N = record
-  { Carrier = M.Carrier × N.Carrier
-  ; _≈_     = Pointwise M._≈_ N._≈_
+  { Carrier = M.Carrier Product.× N.Carrier
+  ; _≈_     = M._≈_ × N._≈_
   ; _∙_     = zip M._∙_ N._∙_
   ; isMagma = record
     { isEquivalence = ×-isEquivalence M.isEquivalence N.isEquivalence

src/Algebra/Construct/LexProduct.agda

@@ -9,8 +9,8 @@
 open import Algebra.Bundles using (Magma)
 open import Algebra.Definitions
 open import Data.Bool.Base using (true; false)
-open import Data.Product.Base using (_×_; _,_)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent using (Pointwise)
+open import Data.Product.Base as Product using (_,_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×_)
 open import Data.Sum.Base using (inj₁; inj₂; map)
 open import Function.Base using (_∘_)
 open import Relation.Binary.Core using (Rel)
@@ -43,8 +43,8 @@ import Algebra.Construct.LexProduct.Inner M N _≟₁_ as InnerLex
 
 private
   infix 4 _≋_
-  _≋_ : Rel (A × B) _
-  _≋_ = Pointwise _≈₁_ _≈₂_
+  _≋_ : Rel (A Product.× B) _
+  _≋_ = _≈₁_ × _≈₂_
 
   variable
     a b : A

src/Algebra/Module/Construct/DirectProduct.agda

@@ -16,7 +16,7 @@ open import Algebra.Construct.DirectProduct using (commutativeMonoid)
 open import Algebra.Module.Bundles
 open import Data.Product.Base using (map; zip; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
-  using (Pointwise)
+  using (_×_)
 open import Level using (Level; _⊔_)
 
 private
@@ -31,7 +31,7 @@ rawLeftSemimodule : {R : Set r} →
                     RawLeftSemimodule R m′ ℓm′ →
                     RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
 rawLeftSemimodule M N = record
-  { _≈ᴹ_ = Pointwise M._≈ᴹ_ N._≈ᴹ_
+  { _≈ᴹ_ = M._≈ᴹ_ × N._≈ᴹ_
   ; _+ᴹ_ = zip M._+ᴹ_ N._+ᴹ_
   ; _*ₗ_ = λ r → map (r M.*ₗ_) (r N.*ₗ_)
   ; 0ᴹ = M.0ᴹ , N.0ᴹ
@@ -52,7 +52,7 @@ rawRightSemimodule : {R : Set r} →
                     RawRightSemimodule R m′ ℓm′ →
                     RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′)
 rawRightSemimodule M N = record
-  { _≈ᴹ_ = Pointwise M._≈ᴹ_ N._≈ᴹ_
+  { _≈ᴹ_ = M._≈ᴹ_ × N._≈ᴹ_
   ; _+ᴹ_ = zip M._+ᴹ_ N._+ᴹ_
   ; _*ᵣ_ = λ mn r → map (M._*ᵣ r) (N._*ᵣ r) mn
   ; 0ᴹ = M.0ᴹ , N.0ᴹ
@@ -72,7 +72,7 @@ rawBisemimodule : {R : Set r} {S : Set s} →
                     RawBisemimodule R S m′ ℓm′ →
                     RawBisemimodule R S (m ⊔ m′) (ℓm ⊔ ℓm′)
 rawBisemimodule M N = record
-  { _≈ᴹ_ = Pointwise M._≈ᴹ_ N._≈ᴹ_
+  { _≈ᴹ_ = M._≈ᴹ_ × N._≈ᴹ_
   ; _+ᴹ_ = zip M._+ᴹ_ N._+ᴹ_
   ; _*ₗ_ = λ r → map (r M.*ₗ_) (r N.*ₗ_)
   ; _*ᵣ_ = λ mn r → map (M._*ᵣ r) (N._*ᵣ r) mn

src/Data/Product/Effectful/Examples.agda

@@ -14,7 +14,7 @@ module Data.Product.Effectful.Examples
 open import Level using (Lift; lift; _⊔_)
 open import Effect.Functor using (RawFunctor)
 open import Effect.Monad using (RawMonad)
-open import Data.Product.Base using (_×_; _,_)
+open import Data.Product.Base as Product using (_,_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Function.Base using (id)
 open import Relation.Binary.Core using (Rel)
@@ -30,32 +30,34 @@ private
 
   module A = Monoid A
 
+  A×B = A.Carrier Product.× Lift a B
+
   open import Data.Product.Effectful.Left A.rawMonoid b
 
-  _≈_ : Rel (A.Carrier × Lift a B) (e ⊔ a ⊔ b)
-  _≈_ = Pointwise A._≈_ _≡_
+  _≈_ : Rel A×B (e ⊔ a ⊔ b)
+  _≈_ = A._≈_ × _≡_
 
   open RawFunctor functor
 
   -- This type to the right of × needs to be a "lifted" version of
   -- (B : Set b) that lives in the universe (Set (a ⊔ b)).
-  fmapIdₗ : (x : A.Carrier × Lift a B) → (id <$> x) ≈ x
+  fmapIdₗ : (x : A×B) → (id <$> x) ≈ x
   fmapIdₗ x = A.refl , refl
 
   open RawMonad monad
 
   -- Now, let's show that "pure" is a unit for >>=. We use Lift in
   -- exactly the same way as above. The data (x : B) then needs to be
   -- "lifted" to this new type (Lift B).
-  pureUnitL : ∀ {x : B} {f : Lift a B → A.Carrier × Lift a B} →
+  pureUnitL : ∀ {x : B} {f : Lift a B → A×B} →
                 (pure (lift x) >>= f) ≈ f (lift x)
   pureUnitL = A.identityˡ _ , refl
 
-  pureUnitR : {x : A.Carrier × Lift a B} → (x >>= pure) ≈ x
+  pureUnitR : {x : A×B} → (x >>= pure) ≈ x
   pureUnitR = A.identityʳ _ , refl
 
   -- And another (limited version of a) monad law...
-  bindCompose : ∀ {f g : Lift a B → A.Carrier × Lift a B} →
-                {x : A.Carrier × Lift a B} →
+  bindCompose : ∀ {f g : Lift a B → A×B} →
+                {x : A×B} →
                 ((x >>= f) >>= g) ≈ (x >>= (λ y → (f y >>= g)))
   bindCompose = A.assoc _ _ _ , refl

src/Data/Product/Function/NonDependent/Propositional.agda

@@ -12,7 +12,7 @@ module Data.Product.Function.NonDependent.Propositional where
 open import Data.Product.Base using (_×_; map)
 open import Data.Product.Function.NonDependent.Setoid
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
-  using (_×ₛ_; Pointwise-≡↔≡)
+  using (_×ₛ_; ×-≡↔≡-×)
 open import Function.Base using (id)
 open import Function.Bundles
   using (Inverse; _⟶_; _⇔_; _↣_; _↠_; _⤖_; _↩_; _↪_; _↔_)
@@ -43,7 +43,7 @@ private
                    R (setoid A) (setoid C) → R (setoid B) (setoid D) →
                    R (setoid (A × B)) (setoid (C × D))
   liftViaInverse trans inv⇒R lift RAC RBD =
-    Inv.transportVia trans inv⇒R (Inv.sym Pointwise-≡↔≡) (lift RAC RBD) Pointwise-≡↔≡
+    Inv.transportVia trans inv⇒R (Inv.sym ×-≡↔≡-×) (lift RAC RBD) ×-≡↔≡-×
 
 ------------------------------------------------------------------------
 -- Combinators for various function types

src/Data/Product/Relation/Binary/Lex/NonStrict.agda

@@ -11,9 +11,9 @@
 
 module Data.Product.Relation.Binary.Lex.NonStrict where
 
-open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Base as Product using (_,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
-  using (Pointwise)
+  using (_×_; _×?_)
 import Data.Product.Relation.Binary.Lex.Strict as Strict
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Level using (Level)
@@ -39,7 +39,7 @@ private
 -- Definition
 
 ×-Lex : (_≈₁_ : Rel A ℓ₁) (_≤₁_ : Rel A ℓ₂) (_≤₂_ : Rel B ℓ₃) →
-        Rel (A × B) _
+        Rel (A Product.× B) _
 ×-Lex _≈₁_ _≤₁_ _≤₂_ = Strict.×-Lex _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_
 
 ------------------------------------------------------------------------
@@ -48,7 +48,7 @@ private
 ×-reflexive : (_≈₁_ : Rel A ℓ₁) (_≤₁_ : Rel A ℓ₂)
               {_≈₂_ : Rel B ℓ₃} (_≤₂_ : Rel B ℓ₄) →
               _≈₂_ ⇒ _≤₂_ →
-              (Pointwise _≈₁_ _≈₂_) ⇒ (×-Lex _≈₁_ _≤₁_ _≤₂_)
+              (_≈₁_ × _≈₂_) ⇒ (×-Lex _≈₁_ _≤₁_ _≤₂_)
 ×-reflexive _≈₁_ _≤₁_ _≤₂_ refl₂ =
   Strict.×-reflexive _≈₁_ (Conv._<_ _≈₁_ _≤₁_) _≤₂_ refl₂
 
@@ -94,7 +94,7 @@ module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
 
   private
     _≤ₗₑₓ_ = ×-Lex _≈₁_ _≤₁_ _≤₂_
-    _≋_    = Pointwise _≈₁_ _≈₂_
+    _≋_    = _≈₁_ × _≈₂_
 
   ×-antisymmetric : IsPartialOrder _≈₁_ _≤₁_ → Antisymmetric _≈₂_ _≤₂_ →
                    Antisymmetric _≋_ _≤ₗₑₓ_
@@ -157,7 +157,7 @@ module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
     { isTotalOrder = ×-isTotalOrder (_≟_ to₁)
                                     (isTotalOrder to₁)
                                     (isTotalOrder to₂)
-    ; _≟_          = Pointwise.×-decidable (_≟_ to₁) (_≟_ to₂)
+    ; _≟_          =(_≟_ to₁) ×? (_≟_ to₂)
     ; _≤?_         = ×-decidable (_≟_ to₁) (_≤?_ to₁) (_≤?_ to₂)
     }
     where open IsDecTotalOrder

src/Data/Product/Relation/Binary/Lex/Strict.agda

@@ -11,9 +11,9 @@
 
 module Data.Product.Relation.Binary.Lex.Strict where
 
-open import Data.Product.Base
+open import Data.Product.Base as Product using (_,_; proj₁; proj₂; _-×-_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
-  using (Pointwise)
+  using (_×_)
 open import Data.Sum.Base using (inj₁; inj₂; _-⊎-_; [_,_])
 open import Function.Base using (flip; _on_; _$_; _∘_)
 open import Induction.WellFounded using (Acc; acc; WfRec; WellFounded; Acc-resp-flip-≈)
@@ -42,7 +42,7 @@ private
 -- A lexicographic ordering over products
 
 ×-Lex : (_≈₁_ : Rel A ℓ₁) (_<₁_ : Rel A ℓ₂) (_≤₂_ : Rel B ℓ₃) →
-        Rel (A × B) _
+        Rel (A Product.× B) _
 ×-Lex _≈₁_ _<₁_ _≤₂_ =
   (_<₁_ on proj₁) -⊎- (_≈₁_ on proj₁) -×- (_≤₂_ on proj₂)
 
@@ -52,7 +52,7 @@ private
 
 ×-reflexive : (_≈₁_ : Rel A ℓ₁) (_∼₁_ : Rel A ℓ₂)
               {_≈₂_ : Rel B ℓ₃} (_≤₂_ : Rel B ℓ₄) →
-              _≈₂_ ⇒ _≤₂_ → (Pointwise _≈₁_ _≈₂_) ⇒ (×-Lex _≈₁_ _∼₁_ _≤₂_)
+              _≈₂_ ⇒ _≤₂_ → (_≈₁_ × _≈₂_) ⇒ (×-Lex _≈₁_ _∼₁_ _≤₂_)
 ×-reflexive _ _ _ refl₂ = λ x≈y →
   inj₂ (proj₁ x≈y , refl₂ (proj₂ x≈y))
 
@@ -120,11 +120,11 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂}
          {_≈₂_ : Rel B ℓ₃} {_<₂_ : Rel B ℓ₄} where
 
   private
-    _≋_    = Pointwise _≈₁_ _≈₂_
+    _≋_    = _≈₁_ × _≈₂_
     _<ₗₑₓ_ = ×-Lex _≈₁_ _<₁_ _<₂_
 
   ×-irreflexive : Irreflexive _≈₁_ _<₁_ → Irreflexive _≈₂_ _<₂_ →
-                  Irreflexive (Pointwise _≈₁_ _≈₂_) _<ₗₑₓ_
+                  Irreflexive (_≈₁_ × _≈₂_) _<ₗₑₓ_
   ×-irreflexive ir₁ ir₂ x≈y (inj₁ x₁<y₁) = ir₁ (proj₁ x≈y) x₁<y₁
   ×-irreflexive ir₁ ir₂ x≈y (inj₂ x≈<y)  = ir₂ (proj₂ x≈y) (proj₂ x≈<y)
 
@@ -230,7 +230,7 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂}
          {_≈₂_ : Rel B ℓ₃} {_<₂_ : Rel B ℓ₄} where
 
   private
-    _≋_    = Pointwise _≈₁_ _≈₂_
+    _≋_    = _≈₁_ × _≈₂_
     _<ₗₑₓ_ = ×-Lex _≈₁_ _<₁_ _<₂_
 
   ×-isPreorder : IsPreorder _≈₁_ _<₁_ →