Equality on dependent function types

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Elisabeth Stenholm and Vojtěch Štěpančík.

Created on 2022-01-31.
Last modified on 2024-03-01.

module foundation.equality-dependent-function-types where
Imports
open import foundation.dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
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-pair-types
open import foundation-core.identity-types
open import foundation-core.torsorial-type-families
open import foundation-core.type-theoretic-principle-of-choice

Idea

Given a family of types B over A, if we can characterize the identity types of each B x, then we can characterize the identity types of (x : A) → B x.

Contractibility

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A  UU l2} {C : (x : A)  B x  UU l3}
  (is-torsorial-C : (x : A)  is-torsorial (C x))
  where

  is-torsorial-Eq-Π : is-torsorial  g  (x : A)  C x (g x))
  is-torsorial-Eq-Π =
    is-contr-equiv'
      ( (x : A)  Σ (B x) (C x))
      ( distributive-Π-Σ)
      ( is-contr-Π is-torsorial-C)

  is-torsorial-Eq-implicit-Π : is-torsorial  g  {x : A}  C x (g {x}))
  is-torsorial-Eq-implicit-Π =
    is-contr-equiv
      ( Σ ((x : A)  B x)  g  (x : A)  C x (g x)))
      ( equiv-Σ
        ( λ g  (x : A)  C x (g x))
        ( equiv-explicit-implicit-Π)
        ( λ _  equiv-explicit-implicit-Π))
      ( is-torsorial-Eq-Π)

Extensionality

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : A  UU l2}
  (f : (x : A)  B x)
  (Eq-B : (x : A)  B x  UU l3)
  where

  map-extensionality-Π :
    ( (x : A) (y : B x)  (f x  y)  Eq-B x y) 
    ( g : (x : A)  B x)  f  g  ((x : A)  Eq-B x (g x))
  map-extensionality-Π e .f refl x = map-equiv (e x (f x)) refl

  abstract
    is-equiv-map-extensionality-Π :
      (e : (x : A) (y : B x)  (f x  y)  Eq-B x y) 
      (g : (x : A)  B x)  is-equiv (map-extensionality-Π e g)
    is-equiv-map-extensionality-Π e =
      fundamental-theorem-id
        ( is-torsorial-Eq-Π
          ( λ x 
            fundamental-theorem-id'
              ( λ y  map-equiv (e x y))
              ( λ y  is-equiv-map-equiv (e x y))))
        ( map-extensionality-Π e)

  extensionality-Π :
    ( (x : A) (y : B x)  (f x  y)  Eq-B x y) 
    ( g : (x : A)  B x)  (f  g)  ((x : A)  Eq-B x (g x))
  pr1 (extensionality-Π e g) = map-extensionality-Π e g
  pr2 (extensionality-Π e g) = is-equiv-map-extensionality-Π e g

See also

Recent changes