Qualified import of Data.Product.Base fixing #2280 (#2284)

* Qualified import of `Data.Product.Base as Product`

* more modules affected

Author: jamesmckinna

src/Algebra/Construct/Flip/Op.agda

@@ -10,7 +10,7 @@
 module Algebra.Construct.Flip.Op where
 
 open import Algebra
-import Data.Product.Base as Prod
+import Data.Product.Base as Product
 import Data.Sum.Base as Sum
 open import Function.Base using (flip)
 open import Level using (Level)
@@ -39,7 +39,7 @@ module _ (≈ : Rel A ℓ) (∙ : Op₂ A) where
   associative sym assoc x y z = sym (assoc z y x)
 
   identity : Identity ≈ ε ∙ → Identity ≈ ε (flip ∙)
-  identity id = Prod.swap id
+  identity id = Product.swap id
 
   commutative : Commutative ≈ ∙ → Commutative ≈ (flip ∙)
   commutative comm = flip comm
@@ -51,7 +51,7 @@ module _ (≈ : Rel A ℓ) (∙ : Op₂ A) where
   idempotent idem = idem
 
   inverse : Inverse ≈ ε ⁻¹ ∙ → Inverse ≈ ε ⁻¹ (flip ∙)
-  inverse inv = Prod.swap inv
+  inverse inv = Product.swap inv
 
 ------------------------------------------------------------------------
 -- Structures

src/Algebra/Construct/Subst/Equality.agda

@@ -9,7 +9,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.Product.Base as Prod
+open import Data.Product.Base as Product
 open import Relation.Binary.Core
 
 module Algebra.Construct.Subst.Equality
@@ -45,13 +45,13 @@ sel : ∀ {∙} → Selective ≈₁ ∙ → Selective ≈₂ ∙
 sel sel x y = Sum.map to to (sel x y)
 
 identity : ∀ {∙ e} → Identity ≈₁ e ∙ → Identity ≈₂ e ∙
-identity = Prod.map (to ∘_) (to ∘_)
+identity = Product.map (to ∘_) (to ∘_)
 
 inverse : ∀ {∙ e ⁻¹} → Inverse ≈₁ ⁻¹ ∙ e → Inverse ≈₂ ⁻¹ ∙ e
-inverse = Prod.map (to ∘_) (to ∘_)
+inverse = Product.map (to ∘_) (to ∘_)
 
 absorptive : ∀ {∙ ◦} → Absorptive ≈₁ ∙ ◦ → Absorptive ≈₂ ∙ ◦
-absorptive = Prod.map (λ f x y → to (f x y)) (λ f x y → to (f x y))
+absorptive = Product.map (λ f x y → to (f x y)) (λ f x y → to (f x y))
 
 distribˡ : ∀ {∙ ◦} → _DistributesOverˡ_ ≈₁ ∙ ◦ → _DistributesOverˡ_ ≈₂ ∙ ◦
 distribˡ distribˡ x y z = to (distribˡ x y z)
@@ -60,7 +60,7 @@ distribʳ : ∀ {∙ ◦} → _DistributesOverʳ_ ≈₁ ∙ ◦ → _Distribute
 distribʳ distribʳ x y z = to (distribʳ x y z)
 
 distrib : ∀ {∙ ◦} → _DistributesOver_ ≈₁ ∙ ◦ → _DistributesOver_ ≈₂ ∙ ◦
-distrib {∙} {◦} = Prod.map (distribˡ {∙} {◦}) (distribʳ {∙} {◦})
+distrib {∙} {◦} = Product.map (distribˡ {∙} {◦}) (distribʳ {∙} {◦})
 
 ------------------------------------------------------------------------
 -- Structures
@@ -92,7 +92,7 @@ isSelectiveMagma S = record
 isMonoid : ∀ {∙ ε} → IsMonoid ≈₁ ∙ ε → IsMonoid ≈₂ ∙ ε
 isMonoid S = record
   { isSemigroup = isSemigroup S.isSemigroup
-  ; identity    = Prod.map (to ∘_) (to ∘_) S.identity
+  ; identity    = Product.map (to ∘_) (to ∘_) S.identity
   } where module S = IsMonoid S
 
 isCommutativeMonoid : ∀ {∙ ε} →
@@ -113,7 +113,7 @@ isIdempotentCommutativeMonoid {∙} S = record
 isGroup : ∀ {∙ ε ⁻¹} → IsGroup ≈₁ ∙ ε ⁻¹ → IsGroup ≈₂ ∙ ε ⁻¹
 isGroup S = record
   { isMonoid = isMonoid S.isMonoid
-  ; inverse  = Prod.map (to ∘_) (to ∘_) S.inverse
+  ; inverse  = Product.map (to ∘_) (to ∘_) S.inverse
   ; ⁻¹-cong  = cong₁ S.⁻¹-cong
   } where module S = IsGroup S
 
@@ -141,7 +141,7 @@ isSemiringWithoutOne {+} {*} S = record
   ; *-cong                = cong₂ S.*-cong
   ; *-assoc               = assoc {*} S.*-assoc
   ; distrib               = distrib {*} {+} S.distrib
-  ; zero                  = Prod.map (to ∘_) (to ∘_) S.zero
+  ; zero                  = Product.map (to ∘_) (to ∘_) S.zero
   } where module S = IsSemiringWithoutOne S
 
 isCommutativeSemiringWithoutOne : ∀ {+ * 0#} →

src/Algebra/Lattice/Construct/Subst/Equality.agda

@@ -12,7 +12,7 @@
 open import Algebra.Core using (Op₂)
 open import Algebra.Definitions
 open import Algebra.Lattice.Structures
-open import Data.Product.Base as Prod
+open import Data.Product.Base using (_,_)
 open import Function.Base
 open import Relation.Binary.Core
 

src/Codata/Musical/Colist.agda

@@ -21,7 +21,7 @@ open import Data.Maybe.Relation.Unary.Any using (just)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.NonEmpty using (List⁺; _∷_)
-open import Data.Product.Base as Prod using (∃; _×_; _,_)
+open import Data.Product.Base as Product using (∃; _×_; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Vec.Bounded as Vec≤ using (Vec≤)
 open import Function.Base
@@ -108,7 +108,7 @@ Any-∈ {P = P} = mk↔ₛ′
   where
   to : ∀ {xs} → Any P xs → ∃ λ x → x ∈ xs × P x
   to (here  p) = _ , here P.refl , p
-  to (there p) = Prod.map id (Prod.map there id) (to p)
+  to (there p) = Product.map id (Product.map there id) (to p)
 
   from : ∀ {x xs} → x ∈ xs → P x → Any P xs
   from (here P.refl) p = here p
@@ -118,7 +118,7 @@ Any-∈ {P = P} = mk↔ₛ′
             to (from x∈xs p) ≡ (x , x∈xs , p)
   to∘from (here P.refl) p = P.refl
   to∘from (there x∈xs)  p =
-    P.cong (Prod.map id (Prod.map there id)) (to∘from x∈xs p)
+    P.cong (Product.map id (Product.map there id)) (to∘from x∈xs p)
 
   from∘to : ∀ {xs} (p : Any P xs) →
             let (x , x∈xs , px) = to p in from x∈xs px ≡ p

src/Codata/Musical/Colist/Infinite-merge.agda

@@ -13,7 +13,7 @@ open import Codata.Musical.Colist as Colist hiding (_⋎_)
 open import Data.Nat.Base
 open import Data.Nat.Induction using (<′-wellFounded)
 open import Data.Nat.Properties
-open import Data.Product.Base as Prod using (_×_; _,_; ∃; ∃₂; proj₁; proj₂)
+open import Data.Product.Base as Product using (_×_; _,_; ∃; ∃₂; proj₁; proj₂)
 open import Data.Sum.Base
 open import Data.Sum.Properties
 open import Data.Sum.Function.Propositional using (_⊎-cong_)
@@ -195,7 +195,7 @@ Any-merge {P = P} xss = mk↔ₛ′ (proj₁ ∘ to xss) from to∘from (proj₂
          | index-Any-⋎P xs p
     ... | inj₁ q | P.refl | _   = here (inj₂ q) , P.refl
     ... | inj₂ q | P.refl | q≤p =
-      Prod.map there
+      Product.map there
                (P.cong (there ∘ (Inverse.from (Any-⋎P xs)) ∘ inj₂))
                (rec (s≤′s q≤p))
 

src/Codata/Sized/Colist/Properties.agda

@@ -27,7 +27,7 @@ open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)
 import Data.Maybe.Properties as Maybeₚ
 open import Data.Maybe.Relation.Unary.All using (All; nothing; just)
 open import Data.Nat.Base as ℕ using (zero; suc; z≤n; s≤s)
-open import Data.Product.Base as Prod using (_×_; _,_; uncurry)
+open import Data.Product.Base as Product using (_×_; _,_; uncurry)
 open import Data.These.Base as These using (These; this; that; these)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Function.Base
@@ -106,7 +106,7 @@ lookup-replicate (suc k) (suc n) a = lookup-replicate k (n .force) a
 -- Properties of unfold
 
 map-unfold : ∀ (f : B → C) (alg : A → Maybe (A × B)) a →
-             i ⊢ map f (unfold alg a) ≈ unfold (Maybe.map (Prod.map₂ f) ∘ alg) a
+             i ⊢ map f (unfold alg a) ≈ unfold (Maybe.map (Product.map₂ f) ∘ alg) a
 map-unfold f alg a with alg a
 ... | nothing       = []
 ... | just (a′ , b) = Eq.refl ∷ λ where .force → map-unfold f alg a′

src/Codata/Sized/Cowriter.agda

@@ -18,7 +18,7 @@ open import Data.Unit.Base
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.NonEmpty.Base using (List⁺; _∷_)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
-open import Data.Product.Base as Prod using (_×_; _,_)
+open import Data.Product.Base as Product using (_×_; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.Vec.Base using (Vec; []; _∷_)
 open import Data.Vec.Bounded.Base as Vec≤ using (Vec≤; _,_)
@@ -68,11 +68,11 @@ length (w ∷ cw) = suc λ where .force → length (cw .force)
 splitAt : ∀ (n : ℕ) → Cowriter W A ∞ → (Vec W n × Cowriter W A ∞) ⊎ (Vec≤ W n × A)
 splitAt zero    cw       = inj₁ ([] , cw)
 splitAt (suc n) [ a ]    = inj₂ (Vec≤.[] , a)
-splitAt (suc n) (w ∷ cw) = Sum.map (Prod.map₁ (w ∷_)) (Prod.map₁ (w Vec≤.∷_))
+splitAt (suc n) (w ∷ cw) = Sum.map (Product.map₁ (w ∷_)) (Product.map₁ (w Vec≤.∷_))
                          $ splitAt n (cw .force)
 
 take : ∀ (n : ℕ) → Cowriter W A ∞ → Vec W n ⊎ (Vec≤ W n × A)
-take n = Sum.map₁ Prod.proj₁ ∘′ splitAt n
+take n = Sum.map₁ Product.proj₁ ∘′ splitAt n
 
 infixr 5 _++_ _⁺++_
 _++_ : ∀ {i} → List W → Cowriter W A i → Cowriter W A i

src/Codata/Sized/M/Properties.agda

@@ -15,7 +15,7 @@ open import Codata.Sized.M
 open import Codata.Sized.M.Bisimilarity
 open import Data.Container.Core as C hiding (map)
 import Data.Container.Morphism as Mp
-open import Data.Product.Base as Prod using (_,_)
+open import Data.Product.Base as Product using (_,_)
 open import Data.Product.Properties hiding (map-cong)
 open import Function.Base using (_$′_; _∘′_)
 import Relation.Binary.PropositionalEquality.Core as P

src/Codata/Sized/Stream/Properties.agda

@@ -20,7 +20,7 @@ open import Data.Nat.GeneralisedArithmetic using (fold; fold-pull)
 open import Data.List.Base as List using ([]; _∷_)
 open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
 import Data.List.Relation.Binary.Equality.Propositional as Eq
-open import Data.Product.Base as Prod using (_,_)
+open import Data.Product.Base as Product using (_,_)
 open import Data.Vec.Base as Vec using (_∷_)
 
 open import Function.Base using (id; _$_; _∘′_; const)
@@ -49,7 +49,7 @@ take-repeat-identity (suc n) a = P.cong (a Vec.∷_) (take-repeat-identity n a)
 
 splitAt-repeat-identity : (n : ℕ) (a : A) → splitAt n (repeat a) ≡ (Vec.replicate n a , repeat a)
 splitAt-repeat-identity zero    a = P.refl
-splitAt-repeat-identity (suc n) a = P.cong (Prod.map₁ (a ∷_)) (splitAt-repeat-identity n a)
+splitAt-repeat-identity (suc n) a = P.cong (Product.map₁ (a ∷_)) (splitAt-repeat-identity n a)
 
 replicate-repeat : ∀ {i} (n : ℕ) (a : A) → i ⊢ List.replicate n a ++ repeat a ≈ repeat a
 replicate-repeat zero    a = refl
@@ -103,10 +103,10 @@ map-∘ f g (a ∷ as) = P.refl ∷ λ where .force → map-∘ f g (as .force)
 -- splitAt
 
 splitAt-map : ∀ n (f : A → B) xs →
-  splitAt n (map f xs) ≡ Prod.map (Vec.map f) (map f) (splitAt n xs)
+  splitAt n (map f xs) ≡ Product.map (Vec.map f) (map f) (splitAt n xs)
 splitAt-map zero    f xs       = P.refl
 splitAt-map (suc n) f (x ∷ xs) =
-  P.cong (Prod.map₁ (f x Vec.∷_)) (splitAt-map n f (xs .force))
+  P.cong (Product.map₁ (f x Vec.∷_)) (splitAt-map n f (xs .force))
 
 ------------------------------------------------------------------------
 -- iterate

src/Data/Container/Core.agda

@@ -9,7 +9,7 @@
 module Data.Container.Core where
 
 open import Level
-open import Data.Product.Base as Prod using (Σ-syntax)
+open import Data.Product.Base as Product using (Σ-syntax)
 open import Function.Base
 open import Function using (Inverse; _↔_)
 open import Relation.Unary using (Pred; _⊆_)
@@ -33,7 +33,7 @@ open Container public
 
 map : ∀ {s p x y} {C : Container s p} {X : Set x} {Y : Set y} →
       (X → Y) → ⟦ C ⟧ X → ⟦ C ⟧ Y
-map f = Prod.map₂ (f ∘_)
+map f = Product.map₂ (f ∘_)
 
 -- Representation of container morphisms.
 
@@ -47,7 +47,7 @@ record _⇒_ {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Containe
     position : ∀ {s} → Position C₂ (shape s) → Position C₁ s
 
   ⟪_⟫ : ∀ {x} {X : Set x} → ⟦ C₁ ⟧ X → ⟦ C₂ ⟧ X
-  ⟪_⟫ = Prod.map shape (_∘′ position)
+  ⟪_⟫ = Product.map shape (_∘′ position)
 
 open _⇒_ public