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
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


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.


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

  multivariable-section : UU (l1  l2)
  multivariable-section =
    Σ ( iterated-Π B  iterated-Π A)
      ( λ s 
          { 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) 
      { n = succ-ℕ n}
      {{A = prepend-telescope (iterated-Π B) B}}
      ( f  map-multivariable-section s)
      ( id)
  is-multivariable-section-map-multivariable-section = pr2

Recent changes