Multivariable sections

Content created by Fredrik Bakke.

Created on 2023-11-24.
Last modified on 2023-12-21.

module foundation.multivariable-sections where

open import foundation.telescopes public
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.iterated-dependent-product-types
open import foundation.multivariable-homotopies
open import foundation.universe-levels

open import foundation-core.function-types

Idea

A multivariable section is a map of multivariable maps that is a right inverse. Thus, a map

  s : ((x₁ : A₁) ... (xₙ : Aₙ) → A x) → (y₁ : B₁) ... (yₙ : Bₙ) → B y

is a section of a map of type

  f : ((y₁ : B₁) ... (yₙ : Bₙ) → B y) → (x₁ : A₁) ... (xₙ : Aₙ) → A x

if the composition f ∘ s is multivariable homotopic to the identity at

  (y₁ : B₁) ... (yₙ : Bₙ) → B y.

Note that sections of multivariable maps are equivalent to common sections by function extensionality, so this definition only finds it utility in avoiding unnecessary applications of function extensionality. For instance, this is useful when defining induction principles on function types.

Definition

module _
  {l1 l2 : Level} (n : ℕ)
  {{A : telescope l1 n}} {{B : telescope l2 n}}
  (f : iterated-Π A → iterated-Π B)
  where

  multivariable-section : UU (l1 ⊔ l2)
  multivariable-section =
    Σ ( iterated-Π B → iterated-Π A)
      ( λ s →
        multivariable-htpy
          { n = succ-ℕ n}
          {{A = prepend-telescope (iterated-Π B) B}}
          ( f ∘ s)
          ( id))

  map-multivariable-section :
    multivariable-section → iterated-Π B → iterated-Π A
  map-multivariable-section = pr1

  is-multivariable-section-map-multivariable-section :
    (s : multivariable-section) →
    multivariable-htpy
      { n = succ-ℕ n}
      {{A = prepend-telescope (iterated-Π B) B}}
      ( f ∘ map-multivariable-section s)
      ( id)
  is-multivariable-section-map-multivariable-section = pr2

Recent changes