Some extra support for homogeneous n-ary products (#2736)

* Some extra support for homogeneous n-ary products

* Update src/Data/Product/Nary/NonDependent.agda

Co-authored-by: jamesmckinna <[email protected]>

---------

Co-authored-by: jamesmckinna <[email protected]>

Author: MatthewDaggitt

CHANGELOG.md

@@ -150,6 +150,11 @@ Deprecated names
   left-inverse ↦ rightInverse
   ```
 
+* In `Data.Product.Nary.NonDependent`:
+  ```agda
+  Allₙ ↦ Pointwiseₙ
+  ```
+
 New modules
 -----------
 
@@ -355,6 +360,12 @@ Additions to existing modules
     LeftInverse (I ×ₛ A) (J ×ₛ B)
   ```
 
+* In `Data.Product.Nary.NonDependent`:
+  ```agda
+  HomoProduct′ n f = Product n (stabulate n (const _) f)
+  HomoProduct  n A = HomoProduct′ n (const A)
+  ```
+
 * In `Data.Vec.Relation.Binary.Pointwise.Inductive`:
   ```agda
   zipWith-assoc : Associative _∼_ f → Associative (Pointwise _∼_) (zipWith {n = n} f)
@@ -364,6 +375,13 @@ Additions to existing modules
   zipWith-cong : Congruent₂ _∼_ f → Pointwise _∼_ ws xs → Pointwise _∼_ ys zs → Pointwise _∼_ (zipWith f ws ys) (zipWith f xs zs)
   ```
 
+* In `Function.Nary.NonDependent.Base`:
+  ```agda
+  lconst l n = ⨆ l (lreplicate l n)
+  stabulate : ∀ n → (f : Fin n → Level) → (g : (i : Fin n) → Set (f i)) → Sets n (ltabulate n f)
+  sreplicate : ∀ n → Set a → Sets n (lreplicate n a)
+  ```
+
 * In `Relation.Binary.Construct.Add.Infimum.Strict`:
   ```agda
   <₋-accessible-⊥₋ : Acc _<₋_ ⊥₋

src/Data/Product/Nary/NonDependent.agda

@@ -46,27 +46,39 @@ Product 0       _        = ⊤
 Product 1       (a , _)  = a
 Product (suc n) (a , as) = a × Product n as
 
--- Pointwise lifting of a relation on products
+-- An n-ary product where every element of the product lives at the same universe level.
 
-Allₙ : (∀ {a} {A : Set a} → Rel A a) →
-        ∀ n {ls} {as : Sets n ls} (l r : Product n as) → Sets n ls
-Allₙ R 0               l       r       = _
-Allₙ R 1               a       b       = R a b , _
-Allₙ R (suc n@(suc _)) (a , l) (b , r) = R a b , Allₙ R n l r
+HomoProduct′ : ∀ n {a} → (Fin n → Set a) → Set (lconst n a)
+HomoProduct′ n f = Product n (stabulate n (const _) f)
+
+-- An n-ary product where every element of the product lives in the same type.
+
+HomoProduct : ∀ n {a} → Set a → Set (lconst n a)
+HomoProduct n A = HomoProduct′ n (const A)
+
+-- Pointwise lifting of a relation over n-ary products
+
+Pointwiseₙ : (∀ {a} {A : Set a} → Rel A a) →
+             ∀ n {ls} {as : Sets n ls} (l r : Product n as) → Sets n ls
+Pointwiseₙ R 0               l       r       = _
+Pointwiseₙ R 1               a       b       = R a b , _
+Pointwiseₙ R (suc n@(suc _)) (a , l) (b , r) = R a b , Pointwiseₙ R n l r
+
+-- Pointwise lifting of propositional equality over n-ary products
 
 Equalₙ : ∀ n {ls} {as : Sets n ls} (l r : Product n as) → Sets n ls
-Equalₙ = Allₙ _≡_
+Equalₙ = Pointwiseₙ _≡_
 
 ------------------------------------------------------------------------
 -- Generic Programs
+------------------------------------------------------------------------
 
 -- Once we have these type definitions, we can write generic programs
 -- over them. They will typically be split into two or three definitions:
 
 -- 1. action on the vector of n levels (if any)
 -- 2. action on the corresponding vector of n Sets
 -- 3. actual program, typed thank to the function defined in step 2.
-------------------------------------------------------------------------
 
 -- see Relation.Binary.PropositionalEquality for congₙ and substₙ, two
 -- equality-related generic programs.
@@ -168,7 +180,6 @@ projₙ : ∀ n {ls} {as : Sets n ls} k → Product n as → Projₙ as k
 projₙ 1               zero    v        = v
 projₙ (suc n@(suc _)) zero    (v , _)  = v
 projₙ (suc n@(suc _)) (suc k) (_ , vs) = projₙ n k vs
-projₙ 1 (suc ()) v
 
 ------------------------------------------------------------------------
 -- zip
@@ -188,41 +199,35 @@ zipWith (suc n@(suc _)) f (v , vs) (w , ws) =
 Levelₙ⁻ : ∀ {n} → Levels n → Fin n → Levels (pred n)
 Levelₙ⁻               (_ , ls) zero    = ls
 Levelₙ⁻ {suc (suc _)} (l , ls) (suc k) = l , Levelₙ⁻ ls k
-Levelₙ⁻ {1} _ (suc ())
 
 Removeₙ : ∀ {n ls} → Sets n ls → ∀ k → Sets (pred n) (Levelₙ⁻ ls k)
 Removeₙ               (_ , as) zero    = as
 Removeₙ {suc (suc _)} (a , as) (suc k) = a , Removeₙ as k
-Removeₙ {1} _ (suc ())
 
 removeₙ : ∀ n {ls} {as : Sets n ls} k →
           Product n as → Product (pred n) (Removeₙ as k)
 removeₙ (suc zero)          zero    _        = _
 removeₙ (suc (suc _))       zero    (_ , vs) = vs
 removeₙ (suc (suc zero))    (suc k) (v , _)  = v
 removeₙ (suc (suc (suc _))) (suc k) (v , vs) = v , removeₙ _ k vs
-removeₙ (suc zero) (suc ()) _
 
 ------------------------------------------------------------------------
 -- insertion of a k-th component
 
 Levelₙ⁺ : ∀ {n} → Levels n → Fin (suc n) → Level → Levels (suc n)
 Levelₙ⁺         ls       zero    l⁺ = l⁺ , ls
 Levelₙ⁺ {suc _} (l , ls) (suc k) l⁺ = l , Levelₙ⁺ ls k l⁺
-Levelₙ⁺ {0} _ (suc ())
 
 Insertₙ : ∀ {n ls l⁺} → Sets n ls → ∀ k (a⁺ : Set l⁺) → Sets (suc n) (Levelₙ⁺ ls k l⁺)
 Insertₙ         as       zero    a⁺ = a⁺ , as
 Insertₙ {suc _} (a , as) (suc k) a⁺ = a , Insertₙ as k a⁺
-Insertₙ {zero} _ (suc ()) _
 
 insertₙ : ∀ n {ls l⁺} {as : Sets n ls} {a⁺ : Set l⁺} k (v⁺ : a⁺) →
           Product n as → Product (suc n) (Insertₙ as k a⁺)
 insertₙ 0               zero    v⁺ vs       = v⁺
 insertₙ (suc n)         zero    v⁺ vs       = v⁺ , vs
 insertₙ 1               (suc k) v⁺ vs       = vs , insertₙ 0 k v⁺ _
 insertₙ (suc n@(suc _)) (suc k) v⁺ (v , vs) = v , insertₙ n k v⁺ vs
-insertₙ 0 (suc ()) _ _
 
 ------------------------------------------------------------------------
 -- update of a k-th component
@@ -240,8 +245,20 @@ updateₙ : ∀ n {ls lᵘ} {as : Sets n ls} k {aᵘ : _ → Set lᵘ} (f : ∀
 updateₙ 1               zero    f v        = f v
 updateₙ (suc (suc _))   zero    f (v , vs) = f v , vs
 updateₙ (suc n@(suc _)) (suc k) f (v , vs) = v , updateₙ n k f vs
-updateₙ 1 (suc ()) _ _
 
 updateₙ′ : ∀ n {ls lᵘ} {as : Sets n ls} k {aᵘ : Set lᵘ} (f : Projₙ as k → aᵘ) →
            Product n as → Product n (Updateₙ as k aᵘ)
 updateₙ′ n k = updateₙ n k
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.3
+
+Allₙ = Pointwiseₙ
+{-# WARNING_ON_USAGE Allₙ
+"Warning: Allₙ was deprecated in v2.3. Please use Pointwiseₙ instead."
+#-}

src/Function/Nary/NonDependent.agda

@@ -22,7 +22,7 @@ open import Data.Product.Nary.NonDependent
   using (Product; uncurryₙ; Equalₙ; curryₙ; fromEqualₙ; toEqualₙ)
 open import Function.Base using (_∘′_; _$′_; const; flip)
 open import Relation.Unary using (IUniversal)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; subst; cong)
 
 private
   variable
@@ -35,19 +35,6 @@ private
 
 open import Function.Nary.NonDependent.Base public
 
-------------------------------------------------------------------------
--- Additional operations on Levels
-
-ltabulate : ∀ n → (Fin n → Level) → Levels n
-ltabulate zero    f = _
-ltabulate (suc n) f = f zero , ltabulate n (f ∘′ suc)
-
-lreplicate : ∀ n → Level → Levels n
-lreplicate n ℓ = ltabulate n (const ℓ)
-
-0ℓs : ∀[ Levels ]
-0ℓs = lreplicate _ 0ℓ
-
 ------------------------------------------------------------------------
 -- Congruence
 

src/Function/Nary/NonDependent/Base.agda

@@ -19,6 +19,8 @@ open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Product.Base using (_×_; _,_)
 open import Data.Unit.Polymorphic.Base using (⊤; tt)
 open import Function.Base using (_∘′_; _$′_; const; flip)
+open import Data.Fin.Base using (Fin; zero; suc)
+open import Relation.Unary using (IUniversal)
 
 private
   variable
@@ -80,6 +82,28 @@ infixr 0 _⇉_
 _⇉_ : ∀ {n ls r} → Sets n ls → Set r → Set (r ⊔ (⨆ n ls))
 _⇉_ = Arrows _
 
+------------------------------------------------------------------------
+-- Operations on Levels
+
+lmap : (Level → Level) → ∀ n → Levels n → Levels n
+lmap f zero    ls       = _
+lmap f (suc n) (l , ls) = f l , lmap f n ls
+
+ltabulate : ∀ n → (Fin n → Level) → Levels n
+ltabulate zero    f = _
+ltabulate (suc n) f = f zero , ltabulate n (f ∘′ suc)
+
+lreplicate : ∀ n → Level → Levels n
+lreplicate n ℓ = ltabulate n (const ℓ)
+
+0ℓs : ∀[ Levels ]
+0ℓs = lreplicate _ 0ℓ
+
+-- Note that you might think that `lconst n l ≡ l`
+-- but unfortunately this isn't true for `n = 0`.
+lconst : ℕ → Level → Level
+lconst l n = ⨆ l (lreplicate l n)
+
 ------------------------------------------------------------------------
 -- Operations on Sets
 
@@ -94,15 +118,21 @@ _<$>_ f {suc n}  (a , as)  = f a , (f <$> as)
 
 -- Level-modifying generalised map
 
-lmap : (Level → Level) → ∀ n → Levels n → Levels n
-lmap f zero    ls       = _
-lmap f (suc n) (l , ls) = f l , lmap f n ls
-
 smap : ∀ f → (∀ {l} → Set l → Set (f l)) →
        ∀ n {ls} → Sets n ls → Sets n (lmap f n ls)
 smap f F zero    as       = _
 smap f F (suc n) (a , as) = F a , smap f F n as
 
+stabulate : ∀ n →
+            (f : Fin n → Level) →
+            (g : (i : Fin n) → Set (f i)) →
+            Sets n (ltabulate n f)
+stabulate ℕ.zero f g = _
+stabulate (suc n) f g = g zero , stabulate n (f ∘′ suc) (λ u → g (suc u))
+
+sreplicate : ∀ n {a} → Set a → Sets n (lreplicate n a)
+sreplicate n A = stabulate n (const _) (const A)
+
 ------------------------------------------------------------------------
 -- Operations on Functions