# Iterated dependent product types

```agda
module foundation.iterated-dependent-product-types where

open import foundation.telescopes public
```

<details><summary>Imports</summary>

```agda
open import elementary-number-theory.natural-numbers

open import foundation.implicit-function-types
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.functoriality-dependent-function-types
open import foundation-core.propositions
open import foundation-core.truncated-types
open import foundation-core.truncation-levels
```

</details>

## Idea

**Iterated dependent products** are defined by iteratively applying the built in
dependent function type operator. More formally, `iterated-Π` is defined as an
operation `telescope l n → UU l` from the type of
[telescopes](foundation.telescopes.md) to the universe of types of universe
level `l`. For example, the iterated dependent product of the telescope

```text
  A₀ : 𝒰 l₀
  A₁ : A₀ → 𝒰 l₁
  A₂ : (x₀ : A₀) → A₁ x₀ → 𝒰 l₂
  A₃ : (x₀ : A₀) (x₁ : A₁ x₀) → A₂ x₀ x₁ → 𝒰 l₃
```

is the dependent product type

```text
  (x₀ : A₀) (x₁ : A₁ x₀) (x₂ : A₂ x₀ x₁) → A₃ x₀ x₁ x₂
```

of universe level `l₀ ⊔ l₁ ⊔ l₂ ⊔ l₃`.

## Definitions

### Iterated dependent products of iterated type families

```agda
iterated-Π :
  {l : Level} {n : }  telescope l n  UU l
iterated-Π (base-telescope A) = A
iterated-Π (cons-telescope {X = X} A) = (x : X)  iterated-Π (A x)

iterated-implicit-Π :
  {l : Level} {n : }  telescope l n  UU l
iterated-implicit-Π (base-telescope A) = A
iterated-implicit-Π (cons-telescope {X = X} A) =
  {x : X}  iterated-implicit-Π (A x)
```

### Iterated sections of type families

```agda
data
  iterated-section : {l : Level} {n : }  telescope l n  UUω
  where
  base-iterated-section :
    {l1 : Level} {A : UU l1}  A  iterated-section (base-telescope A)
  cons-iterated-section :
    {l1 l2 : Level} {n : } {X : UU l1} {Y : X  telescope l2 n} 
    ((x : X)  iterated-section (Y x))  iterated-section (cons-telescope Y)
```

### Iterated λ-abstractions

```agda
iterated-λ :
  {l : Level} {n : } {A : telescope l n} 
  iterated-section A  iterated-Π A
iterated-λ (base-iterated-section a) = a
iterated-λ (cons-iterated-section f) x = iterated-λ (f x)
```

### Transforming iterated products

Given an operation on universes, we can apply it at the codomain of the iterated
product.

```agda
apply-codomain-iterated-Π :
  {l1 : Level} {n : }
  (P : {l : Level}  UU l  UU l)  telescope l1 n  UU l1
apply-codomain-iterated-Π P A = iterated-Π (apply-base-telescope P A)

apply-codomain-iterated-implicit-Π :
  {l1 : Level} {n : }
  (P : {l : Level}  UU l  UU l)  telescope l1 n  UU l1
apply-codomain-iterated-implicit-Π P A =
  iterated-implicit-Π (apply-base-telescope P A)
```

## Properties

### If a dependent product satisfies a property if its codomain does, then iterated dependent products satisfy that property if the codomain does

```agda
section-iterated-Π-section-Π-section-codomain :
  (P : {l : Level}  UU l  UU l) 
  ( {l1 l2 : Level} {A : UU l1} {B : A  UU l2} 
    ((x : A)  P (B x))  P ((x : A)  B x)) 
  {l : Level} (n : ) {{A : telescope l n}} 
  apply-codomain-iterated-Π P A  P (iterated-Π A)
section-iterated-Π-section-Π-section-codomain P f ._ {{base-telescope A}} H =
  H
section-iterated-Π-section-Π-section-codomain P f ._ {{cons-telescope A}} H =
  f  x  section-iterated-Π-section-Π-section-codomain P f _ {{A x}} (H x))

section-iterated-implicit-Π-section-Π-section-codomain :
  (P : {l : Level}  UU l  UU l) 
  ( {l1 l2 : Level} {A : UU l1} {B : A  UU l2} 
    ((x : A)  P (B x))  P ({x : A}  B x)) 
  {l : Level} (n : ) {{A : telescope l n}} 
  apply-codomain-iterated-Π P A  P (iterated-implicit-Π A)
section-iterated-implicit-Π-section-Π-section-codomain
  P f ._ {{base-telescope A}} H =
  H
section-iterated-implicit-Π-section-Π-section-codomain
  P f ._ {{cons-telescope A}} H =
  f ( λ x 
      section-iterated-implicit-Π-section-Π-section-codomain
        P f _ {{A x}} (H x))
```

### Multivariable function types are equivalent to multivariable implicit function types

```agda
equiv-explicit-implicit-iterated-Π :
  {l : Level} (n : ) {{A : telescope l n}} 
  iterated-implicit-Π A  iterated-Π A
equiv-explicit-implicit-iterated-Π .0  base-telescope A  = id-equiv
equiv-explicit-implicit-iterated-Π ._  cons-telescope A  =
  equiv-Π-equiv-family  x  equiv-explicit-implicit-iterated-Π _ {{A x}}) ∘e
  equiv-explicit-implicit-Π

equiv-implicit-explicit-iterated-Π :
  {l : Level} (n : ) {{A : telescope l n}} 
  iterated-Π A  iterated-implicit-Π A
equiv-implicit-explicit-iterated-Π n {{A}} =
  inv-equiv (equiv-explicit-implicit-iterated-Π n {{A}})
```

### Iterated products of contractible types is contractible

```agda
is-contr-iterated-Π :
  {l : Level} (n : ) {{A : telescope l n}} 
  apply-codomain-iterated-Π is-contr A  is-contr (iterated-Π A)
is-contr-iterated-Π =
  section-iterated-Π-section-Π-section-codomain is-contr is-contr-Π

is-contr-iterated-implicit-Π :
  {l : Level} (n : ) {{A : telescope l n}} 
  apply-codomain-iterated-Π is-contr A  is-contr (iterated-implicit-Π A)
is-contr-iterated-implicit-Π =
  section-iterated-implicit-Π-section-Π-section-codomain
    ( is-contr)
    ( is-contr-implicit-Π)
```

### Iterated products of propositions are propositions

```agda
is-prop-iterated-Π :
  {l : Level} (n : ) {{A : telescope l n}} 
  apply-codomain-iterated-Π is-prop A  is-prop (iterated-Π A)
is-prop-iterated-Π =
  section-iterated-Π-section-Π-section-codomain is-prop is-prop-Π

is-prop-iterated-implicit-Π :
  {l : Level} (n : ) {{A : telescope l n}} 
  apply-codomain-iterated-Π is-prop A  is-prop (iterated-implicit-Π A)
is-prop-iterated-implicit-Π =
  section-iterated-implicit-Π-section-Π-section-codomain is-prop is-prop-Π'
```

### Iterated products of truncated types are truncated

```agda
is-trunc-iterated-Π :
  {l : Level} (k : 𝕋) (n : ) {{A : telescope l n}} 
  apply-codomain-iterated-Π (is-trunc k) A  is-trunc k (iterated-Π A)
is-trunc-iterated-Π k =
  section-iterated-Π-section-Π-section-codomain (is-trunc k) (is-trunc-Π k)
```

## See also

- [Iterated Σ-types](foundation.iterated-dependent-pair-types.md)
- [Multivariable homotopies](foundation.multivariable-homotopies.md)