関数の外延性

module foundations.function-extensionality where

open import foundations.universe
open import foundations.identity-type
open import foundations.homotopy
open import foundations.bi-invertible-map
open import foundations.happly
open import foundations.quasi-inverse-to-bi-invertible-map
open import foundations.bi-invertible-map-to-quasi-inverse
open import foundations.quasi-inverse
open import foundations.sigma-type
open import foundations.function
open import foundations.equivalence-is-equivalence-relation
open import foundations.identity-type-respects-equivalence
open import foundations.implicit-function
open import foundations.functions-are-functors

関数の外延性は素のAgdaでは示すことができない。したがって、その型のみ定義しておく。

private variable
  ℓ ℓ′ : Level

FunExtType : (A : Type ℓ) → (A → Type ℓ′) → Type (ℓ ⊔ ℓ′)
FunExtType A B = ∀ (f g : (a : A) → B a) → biinv (happly {f = f} {g = g})

FunExtLevel : ∀ ℓ ℓ′ → Type (lsuc (ℓ ⊔ ℓ′))
FunExtLevel ℓ ℓ′ = ∀ {A : Type ℓ} {B : A → Type ℓ′} → FunExtType A B

FunExtAll : Typeω
FunExtAll = ∀ {ℓ ℓ′} → FunExtLevel ℓ ℓ′

module _ {A : Type ℓ} {B : A → Type ℓ′} (e : FunExtType A B) where
  byFunExtType : (f g : (a : A) → B a) → f ~ g → f ＝ g
  byFunExtType f g = e f g .fst .fst

  retractByFunExtType : (f g : (a : A) → B a)
    → byFunExtType f g ∘ happly ~ idFunction (f ＝ g)
  retractByFunExtType f g = e f g .fst .snd

  sectionByFunExtType : (f g : (a : A) → B a)
    → happly ∘ byFunExtType f g ~ idFunction (f ~ g)
  sectionByFunExtType f g = biinv⇒QuasiInv (e f g) .QuasiInv.rinv

  funExtImplicit : ∀ (f g : {a : A} → B a) → (Id ({a : A} → B a) f g) ≃ (∀ (a : A) → f {a = a} ＝ g)
  funExtImplicit f g =
    trans≃
      (ap toExplicitΠ , idRespEquiv toExplicitΠ (sym≃ explicitΠ≃implicitΠ .snd) f g)
      (trans≃ (happly , e _ _) (idFunction _ ,
                                  ((idFunction _ , (λ _ → refl)) , (idFunction _ , (λ _ → refl)))))

  byFunExtImplicit : (f g : {a : A} → B a) → (∀ (a : A) → f {a = a} ＝ g) → Id ({a : A} → B a) f g
  byFunExtImplicit f g = funExtImplicit f g .snd .fst .fst