open import 1Lab.Prelude

open import Data.Fin.Base

module Data.Fin.Product where

Finitary dependent products🔗

This module defines the product of a finite sequence of types, along with strictly curried (non-dependent) functions whose domain is a finite product. The construction is maximally universe-polymorphic, in that it supports sequences whose universe level varies between components, and is valued in their finite supremum, giving universes for products more precise than Setω.

ℓ-maxᶠ : ∀ {n} (ℓ : Fin n → Level) → Level
ℓ-maxᶠ {n = zero} ℓ = lzero
ℓ-maxᶠ {n = suc n} ℓ = ℓ fzero ⊔ ℓ-maxᶠ (λ i → ℓ (fsuc i))

We define the product of a sequence $P\text{,}$ ${\Pi }^{f}P\text{,}$ by recursion on the number of elements: the empty product is the unit type by decree, and the product of a nonempty sequence is the (binary) product of its head and the $n\text{-ary}$ product of its tail.

Πᶠ : ∀ {n ℓ} (P : (i : Fin n) → Type (ℓ i)) → Type (ℓ-maxᶠ ℓ)
Πᶠ {n = } P     = ⊤
Πᶠ {n = suc n} P = P fzero × Πᶠ λ i → P (fsuc i)

Note that we can define functions converting between the types ${\Pi }^{f}P$ and ${\prod }_{i:[n]}P(i)\text{.}$ However, since this latter type lives in a limit universe when $P$ has non-constant level, we can not express that these functions are isomorphisms in full generality.

indexₚ : ∀ {n ℓ} {P : (i : Fin n) → Type (ℓ i)}
       → Πᶠ {ℓ = ℓ} P → ∀ i → P i
indexₚ {n = zero}  {P = P} prod ()
indexₚ {n = suc n} {P = P} prod fzero = prod .fst
indexₚ {n = suc n} {P = P} prod (fsuc x) = indexₚ (prod .snd) x

tabulateₚ
  : ∀ {n} {ℓ : Fin n → Level} {P : (i : Fin n) → Type (ℓ i)}
  → (∀ i → P i) → Πᶠ P
tabulateₚ {n = zero} f  = tt
tabulateₚ {n = suc n} f = f fzero , tabulateₚ λ i → f (fsuc i)

Elements of ${\Pi }^f$ for sequences with a known length enjoy strong extensionality properties, since they are iterated types with $\eta \text{-expansion.}$ As an example:

module _ {ℓ : Fin  → Level} {P : (i : Fin ) → Type (ℓ i)} where

  _ : {p : Πᶠ {n = } P} → p ≡ (p .fst , p .snd .fst , p .snd .snd .fst , tt)
  _ = refl

Exploiting this structure, we can establish that a product has h-level $k$ when all of its factors do.

Πᶠ-is-hlevel
  : ∀ {n ℓ} {P : (i : Fin n) → Type (ℓ i)} k
  → (∀ i → is-hlevel (P i) k) → is-hlevel (Πᶠ {ℓ = ℓ} P) k
Πᶠ-is-hlevel {n = } {P = P} zero hl    = hlevel 
Πᶠ-is-hlevel {n = } {P = P} (suc k) hl = is-prop→is-hlevel-suc (λ _ _ _ → tt)

Πᶠ-is-hlevel {n = suc n} {P = P} k hl = ×-is-hlevel k (hl fzero) $
  Πᶠ-is-hlevel {P = λ i → P (fsuc i)} k (λ i → hl (fsuc i))

More concretely, we can treat these products as data structures, and update a single value, by index; Or alter the entire tuple using a sequence of functions. Moreover, these functions have their expected behaviour, and, when the length of the sequence is a numeral, will simply compute away.

updateₚ
  : ∀ {n} {ℓ : Fin n → Level} {P : (i : Fin n) → Type (ℓ i)}
  → Πᶠ P → ∀ i → P i → Πᶠ P
updateₚ xs fzero x    = x , xs .snd
updateₚ xs (fsuc k) x = xs .fst , updateₚ (xs .snd) k x

mapₚ
  : ∀ {n} {ℓ ℓ' : Fin n → Level}
      {P : (i : Fin n) → Type (ℓ i)}
      {Q : (i : Fin n) → Type (ℓ' i)}
  → (∀ i → P i → Q i) → Πᶠ P → Πᶠ Q
mapₚ {}     f xs = xs
mapₚ {suc n} f xs = f fzero (xs .fst) , mapₚ (λ i → f (fsuc i)) (xs .snd)

More generically, we can characterise the entries of an updated product type.

updatedₚ
 : ∀ {n} {ℓ : Fin (suc n) → Level} {P : (i : Fin (suc n)) → Type (ℓ i)}
 → (p : Πᶠ P) (i : Fin (suc n)) (x : P i)
 → (indexₚ {P = P} (updateₚ {P = P} p i x) i) ≡ x
updatedₚ {zero}  p fzero x    = refl
updatedₚ {suc n} p fzero x    = refl
updatedₚ {suc n} p (fsuc i) x = updatedₚ (p .snd) i x

updated-neₚ
 : ∀ {n} {ℓ : Fin (suc n) → Level} {P : (i : Fin (suc n)) → Type (ℓ i)}
 → (p : Πᶠ P) (i j : Fin (suc n)) (x : P i)
 → (i ≡ j → ⊥)
 → indexₚ {P = P} (updateₚ {P = P} p i x) j ≡ indexₚ {P = P} p j
updated-neₚ {zero}  p fzero    fzero    x i≠j = absurd (i≠j refl)
updated-neₚ {suc n} p fzero    fzero    x i≠j = absurd (i≠j refl)
updated-neₚ {suc n} p fzero    (fsuc j) x i≠j = refl
updated-neₚ {suc n} p (fsuc i) fzero    x i≠j = refl
updated-neₚ {suc n} p (fsuc i) (fsuc j) x i≠j = updated-neₚ (p .snd) i j x λ p → i≠j (ap fsuc p)

Finitary curried functions🔗

In addition to the finitary dependent products, we can define the type of strictly curried functions as a more convenient alternative for non-dependent functions of type $({\Pi }^{f}P)\to X\text{.}$ Rather than taking their arguments as tuples, finitary curried functions are… curried.

Arrᶠ : ∀ {n ℓ ℓ'} (P : (i : Fin n) → Type (ℓ i)) → Type ℓ' → Type (ℓ-maxᶠ ℓ ⊔ ℓ')
Arrᶠ {} P x     = x
Arrᶠ {suc n} P x = P fzero → Arrᶠ (λ i → P (fsuc i)) x

In the generic case, a finitary curried function can be eliminated using a finitary dependent product; Moreover, curried functions are “extensional” with respect to this application.

applyᶠ
  : ∀ {n ℓ'} {ℓ : Fin n → Level} {P : (i : Fin n) → Type (ℓ i)} {X : Type ℓ'}
  → Arrᶠ P X → Πᶠ P → X
applyᶠ {} f as           = f
applyᶠ {suc n} f (a , as) = applyᶠ (f a) as

funextᶠ
  : ∀ {n ℓ'} {ℓ : Fin n → Level} {P : (i : Fin n) → Type (ℓ i)} {X : Type ℓ'}
  → {f g : Arrᶠ P X} → (∀ (as : Πᶠ P) → applyᶠ f as ≡ applyᶠ g as)
  → f ≡ g
funextᶠ {n = }     ps = ps tt
funextᶠ {n = suc n} ps = funext λ x → funextᶠ λ r → ps (x , r)

Arrᶠ-is-hlevel
  : ∀ {n ℓ'} {ℓ : Fin n → Level} {P : (i : Fin n) → Type (ℓ i)} {X : Type ℓ'}
  → ∀ k → is-hlevel X k → is-hlevel (Arrᶠ P X) k
Arrᶠ-is-hlevel {n = zero}          k hl = hl
Arrᶠ-is-hlevel {n = suc n} {P = P} k hl = fun-is-hlevel k $
  Arrᶠ-is-hlevel {P = λ i → P (fsuc i)} k hl

Other than characterising the identity types of finitary curried functions, we shall need combinators for defining constant functions, for post-composition with an ordinary function, and for “zipping” two functions together (applying a binary operation pointwise).

zipᶠ
  : ∀ {n ℓ' ℓ'' ℓ'''} {ℓ : Fin n → Level} {P : (i : Fin n) → Type (ℓ i)}
      {X : Type ℓ'} {Y : Type ℓ''} {Z : Type ℓ'''}
  → (X → Y → Z) → Arrᶠ P X → Arrᶠ P Y → Arrᶠ P Z
zipᶠ {n = zero}  f g h   = f g h
zipᶠ {n = suc n} f g h a = zipᶠ f (g a) (h a)

mapᶠ
  : ∀ {n ℓ' ℓ''} {ℓ : Fin n → Level} {P : (i : Fin n) → Type (ℓ i)}
      {X : Type ℓ'} {Y : Type ℓ''}
  → (X → Y) → Arrᶠ P X → Arrᶠ P Y
mapᶠ {n = }     f g   = f g
mapᶠ {n = suc n} f g x = mapᶠ f (g x)

constᶠ
  : ∀ {n ℓ'} {ℓ : Fin n → Level} {P : (i : Fin n) → Type (ℓ i)} {X : Type ℓ'}
  → X → Arrᶠ P X
constᶠ {n = }     x   = x
constᶠ {n = suc n} x _ = constᶠ x

Again, when the length is a numeral, these operations are forced to compute to the expected expressions by the computation of their type. However, in the generic case, we must express the computation rules propositionally. Fortunately, simple inductive arguments suffice to prove them.

apply-constᶠ
  : ∀ {n ℓ'} {ℓ : Fin n → Level} {P : (i : Fin n) → Type (ℓ i)} {X : Type ℓ'}
    (x : X) (as : Πᶠ P)
  → applyᶠ (constᶠ x) as ≡ x
apply-constᶠ {n = }     x as = refl
apply-constᶠ {n = suc n} x as = apply-constᶠ x (as .snd)

apply-zipᶠ
  : ∀ {n ℓ' ℓ'' ℓ'''} {ℓ : Fin n → Level} {P : (i : Fin n) → Type (ℓ i)}
      {X : Type ℓ'} {Y : Type ℓ''} {Z : Type ℓ'''}
    (f : X → Y → Z) (g : Arrᶠ P X) (h : Arrᶠ P Y) (as : Πᶠ P)
  → applyᶠ (zipᶠ f g h) as ≡ f (applyᶠ g as) (applyᶠ h as)
apply-zipᶠ {n = }     f g h as = refl
apply-zipᶠ {n = suc n} f g h as = apply-zipᶠ f (g (as .fst)) (h (as .fst)) (as .snd)

apply-mapᶠ
  : ∀ {n ℓ' ℓ''} {ℓ : Fin n → Level} {P : (i : Fin n) → Type (ℓ i)}
      {X : Type ℓ'} {Y : Type ℓ''}
    (f : X → Y) (g : Arrᶠ P X) (as : Πᶠ P)
  → applyᶠ (mapᶠ f g) as ≡ f (applyᶠ g as)
apply-mapᶠ {n = }     f g as = refl
apply-mapᶠ {n = suc n} f g as = apply-mapᶠ f (g (as .fst)) (as .snd)