Iterated dependent product types

Content created by Fredrik Bakke, Egbert Rijke and Vojtěch Štěpančík.

Created on 2023-10-22.
Last modified on 2024-01-11.

module foundation.iterated-dependent-product-types where

open import foundation.telescopes public
Imports 
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

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 to the universe of types of universe level l. For example, the iterated dependent product of the telescope

  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

  (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

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

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

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.

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

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 .0 {{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 .0 {{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

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

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

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-implicit-Π)

Iterated products of truncated types are truncated

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

Recent changes