Skip to content

Some extra support for homogeneous n-ary products #2736

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jun 30, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 18 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -150,6 +150,11 @@ Deprecated names
left-inverse ↦ rightInverse
```

* In `Data.Product.Nary.NonDependent`:
```agda
Allₙ ↦ Pointwiseₙ
```

New modules
-----------

Expand Down Expand Up @@ -296,6 +301,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)
Expand All @@ -305,6 +316,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 _<₋_ ⊥₋
Expand Down
49 changes: 33 additions & 16 deletions src/Data/Product/Nary/NonDependent.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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."
#-}
15 changes: 1 addition & 14 deletions src/Function/Nary/NonDependent.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

Expand Down
38 changes: 34 additions & 4 deletions src/Function/Nary/NonDependent/Base.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand All @@ -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

Expand Down