This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.
Iterated dependent product types
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)