Qualified import of Data.Product.Base fixing #2280

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
 

src/Data/Fin/Properties.agda

@@ -23,7 +23,7 @@ open import Data.Nat.Base as ℕ
 import Data.Nat.Properties as ℕ
 open import Data.Nat.Solver
 open import Data.Unit using (⊤; tt)
-open import Data.Product.Base as Prod
+open import Data.Product.Base as Product
   using (∃; ∃₂; _×_; _,_; map; proj₁; proj₂; uncurry; <_,_>)
 open import Data.Product.Properties using (,-injective)
 open import Data.Product.Algebra using (×-cong)
@@ -644,7 +644,7 @@ splitAt-≥ (suc m) (suc i) i≥m = cong (Sum.map suc id) (splitAt-≥ m i (ℕ.
 remQuot-combine : ∀ {n k} (i : Fin n) j → remQuot k (combine i j) ≡ (i , j)
 remQuot-combine {suc n} {k} zero    j rewrite splitAt-↑ˡ k j (n ℕ.* k) = refl
 remQuot-combine {suc n} {k} (suc i) j rewrite splitAt-↑ʳ k   (n ℕ.* k) (combine i j) =
-  cong (Prod.map₁ suc) (remQuot-combine i j)
+  cong (Product.map₁ suc) (remQuot-combine i j)
 
 combine-remQuot : ∀ {n} k (i : Fin (n ℕ.* k)) → uncurry combine (remQuot {n} k i) ≡ i
 combine-remQuot {suc n} k i with splitAt k i in eq

src/Data/List/Base.agda

@@ -17,7 +17,7 @@ open import Data.Bool.Base as Bool
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _*_ ; _≤_ ; s≤s)
-open import Data.Product.Base as Prod using (_×_; _,_; map₁; map₂′)
+open import Data.Product.Base as Product using (_×_; _,_; map₁; map₂′)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
 open import Function.Base
@@ -96,13 +96,13 @@ zipWith f _        _        = []
 unalignWith : (A → These B C) → List A → List B × List C
 unalignWith f []       = [] , []
 unalignWith f (a ∷ as) with f a
-... | this b    = Prod.map₁ (b ∷_) (unalignWith f as)
-... | that c    = Prod.map₂ (c ∷_) (unalignWith f as)
-... | these b c = Prod.map (b ∷_) (c ∷_) (unalignWith f as)
+... | this b    = Product.map₁ (b ∷_) (unalignWith f as)
+... | that c    = Product.map₂ (c ∷_) (unalignWith f as)
+... | these b c = Product.map (b ∷_) (c ∷_) (unalignWith f as)
 
 unzipWith : (A → B × C) → List A → List B × List C
 unzipWith f []         = [] , []
-unzipWith f (xy ∷ xys) = Prod.zip _∷_ _∷_ (f xy) (unzipWith f xys)
+unzipWith f (xy ∷ xys) = Product.zip _∷_ _∷_ (f xy) (unzipWith f xys)
 
 partitionSumsWith : (A → B ⊎ C) → List A → List B × List C
 partitionSumsWith f = unalignWith (These.fromSum ∘′ f)
@@ -340,7 +340,7 @@ drop (suc n) (x ∷ xs) = drop n xs
 splitAt : ℕ → List A → List A × List A
 splitAt zero    xs       = ([] , xs)
 splitAt (suc n) []       = ([] , [])
-splitAt (suc n) (x ∷ xs) = Prod.map₁ (x ∷_) (splitAt n xs)
+splitAt (suc n) (x ∷ xs) = Product.map₁ (x ∷_) (splitAt n xs)
 
 removeAt : (xs : List A) → Fin (length xs) → List A
 removeAt (x ∷ xs) zero     = xs
@@ -406,7 +406,7 @@ partitionᵇ p = partition (T? ∘ p)
 span : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A)
 span P? []       = ([] , [])
 span P? ys@(x ∷ xs) with does (P? x)
-... | true  = Prod.map (x ∷_) id (span P? xs)
+... | true  = Product.map (x ∷_) id (span P? xs)
 ... | false = ([] , ys)
 
 

src/Data/List/Membership/Propositional/Properties/Core.agda

@@ -17,7 +17,7 @@ open import Function.Bundles
 open import Data.List.Base using (List)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.List.Membership.Propositional
-open import Data.Product.Base as Prod
+open import Data.Product.Base as Product
   using (_,_; proj₁; proj₂; uncurry′; ∃; _×_)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core as P
@@ -42,7 +42,7 @@ map∘find (there p) hyp = P.cong there (map∘find p hyp)
 
 find∘map : ∀ {P : Pred A p} {Q : Pred A q}
            {xs : List A} (p : Any P xs) (f : P ⊆ Q) →
-           find (Any.map f p) ≡ Prod.map id (Prod.map id f) (find p)
+           find (Any.map f p) ≡ Product.map id (Product.map id f) (find p)
 find∘map (here  p) f = refl
 find∘map (there p) f rewrite find∘map p f = refl
 

src/Data/List/Membership/Setoid.agda

@@ -15,7 +15,7 @@ open import Function.Base using (_∘_; id; flip)
 open import Data.List.Base as List using (List; []; _∷_; length; lookup)
 open import Data.List.Relation.Unary.Any as Any
   using (Any; index; map; here; there)
-open import Data.Product.Base as Prod using (∃; _×_; _,_)
+open import Data.Product.Base as Product using (∃; _×_; _,_)
 open import Relation.Unary using (Pred)
 open import Relation.Nullary.Negation using (¬_)
 
@@ -50,7 +50,7 @@ module _ {p} {P : Pred A p} where
 
   find : ∀ {xs} → Any P xs → ∃ λ x → x ∈ xs × P x
   find (here px)   = (_ , here refl , px)
-  find (there pxs) = Prod.map id (Prod.map there id) (find pxs)
+  find (there pxs) = Product.map id (Product.map there id) (find pxs)
 
   lose : P Respects _≈_ →  ∀ {x xs} → x ∈ xs → P x → Any P xs
   lose resp x∈xs px = map (flip resp px) x∈xs

src/Data/List/Membership/Setoid/Properties.agda

@@ -21,7 +21,7 @@ import Data.List.Relation.Binary.Equality.Setoid as Equality
 import Data.List.Relation.Unary.Unique.Setoid as Unique
 open import Data.Nat.Base using (suc; z≤n; s≤s; _≤_; _<_)
 open import Data.Nat.Properties using (≤-trans; n≤1+n)
-open import Data.Product.Base as Prod using (∃; _×_; _,_ ; ∃₂; proj₁; proj₂)
+open import Data.Product.Base as Product using (∃; _×_; _,_ ; ∃₂; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (_$_; flip; _∘_; _∘′_; id)
@@ -342,10 +342,10 @@ module _ (S : Setoid c ℓ) {P : Pred (Carrier S) p}
 
   ∈-filter⁻ : ∀ {v xs} → v ∈ filter P? xs → v ∈ xs × P v
   ∈-filter⁻ {xs = x ∷ xs} v∈f[x∷xs] with P? x
-  ... | false because  _   = Prod.map there id (∈-filter⁻ v∈f[x∷xs])
+  ... | false because  _   = Product.map there id (∈-filter⁻ v∈f[x∷xs])
   ... |  true because [Px] with v∈f[x∷xs]
   ...   | here  v≈x   = here v≈x , resp (sym v≈x) (invert [Px])
-  ...   | there v∈fxs = Prod.map there id (∈-filter⁻ v∈fxs)
+  ...   | there v∈fxs = Product.map there id (∈-filter⁻ v∈fxs)
 
 ------------------------------------------------------------------------
 -- derun and deduplicate

src/Data/List/Nary/NonDependent.agda

@@ -10,7 +10,7 @@ module Data.List.Nary.NonDependent where
 
 open import Data.Nat.Base using (zero; suc)
 open import Data.List.Base as List using (List; []; _∷_)
-open import Data.Product.Base as Prod using (_,_)
+open import Data.Product.Base as Product using (_,_)
 open import Data.Product.Nary.NonDependent using (Product)
 open import Function.Base using ()
 open import Function.Nary.NonDependent.Base
@@ -37,7 +37,7 @@ zipWith : ∀ n {ls} {as : Sets n ls} {r} {R : Set r} →
 zipWith 0               f       = []
 zipWith 1               f xs    = List.map f xs
 zipWith (suc n@(suc _)) f xs ys =
-  zipWith n (Prod.uncurry f) (List.zipWith _,_ xs ys)
+  zipWith n (Product.uncurry f) (List.zipWith _,_ xs ys)
 
 unzipWith : ∀ n {ls} {as : Sets n ls} {a} {A : Set a} →
             (A → Product n as) → (List A → Product n (List <$> as))