Formulation of function extensionality

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module UF-FunExt where

open import SpartanMLTT
open import UF-Base
open import UF-Equiv
open import UF-LeftCancellable

\end{code}

The appropriate notion of function extensionality in univalent
mathematics is funext, define below. It is implied, by an argument due
to Voevodky, by naive, non-dependent function extensionality, written
naive-funext here.

\begin{code}

naive-funext : โˆ€ ๐“ค ๐“ฅ โ†’ ๐“ค โบ โŠ” ๐“ฅ โบ ฬ‡
naive-funext ๐“ค ๐“ฅ = {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡} {f g : X โ†’ Y} โ†’ f โˆผ g โ†’ f โ‰ก g

DN-funext : โˆ€ ๐“ค ๐“ฅ โ†’ ๐“ค โบ โŠ” ๐“ฅ โบ ฬ‡
DN-funext ๐“ค ๐“ฅ = {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡} {f g : ฮ  A} โ†’ f โˆผ g โ†’ f โ‰ก g

funext : โˆ€ ๐“ค ๐“ฅ โ†’ ๐“ค โบ โŠ” ๐“ฅ โบ ฬ‡
funext ๐“ค ๐“ฅ = {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡} (f g : ฮ  A) โ†’ is-equiv (happly' f g)

FunExt : ๐“คฯ‰
FunExt = (๐“ค ๐“ฅ : Universe) โ†’ funext ๐“ค ๐“ฅ

FunExt' : ๐“คฯ‰
FunExt' = {๐“ค ๐“ฅ : Universe} โ†’ funext ๐“ค ๐“ฅ

โ‰ƒ-funext : funext ๐“ค ๐“ฅ โ†’ {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡} (f g : ฮ  A)
         โ†’ (f โ‰ก g) โ‰ƒ (f โˆผ g)
โ‰ƒ-funext fe f g = happly' f g , fe f g

dfunext : funext ๐“ค ๐“ฅ โ†’ DN-funext ๐“ค ๐“ฅ
dfunext fe {X} {A} {f} {g} = prโ‚(prโ‚(fe f g))

nfunext : funext ๐“ค ๐“ฅ โ†’ naive-funext ๐“ค ๐“ฅ
nfunext fe = dfunext fe

happly-funext : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡}
                (fe : funext ๐“ค ๐“ฅ) (f g : ฮ  A) (h : f โˆผ g)
              โ†’ happly (dfunext fe h) โ‰ก h
happly-funext fe f g = prโ‚‚(prโ‚(fe f g))

funext-lc : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡} (fe : funext ๐“ค ๐“ฅ)
         โ†’ (f g : ฮ  A) โ†’ left-cancellable (dfunext fe {X} {A} {f} {g})
funext-lc fe f g = section-lc (dfunext fe) (happly , happly-funext fe f g)

happly-lc : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡} (fe : funext ๐“ค ๐“ฅ) (f g : ฮ  A)
         โ†’ left-cancellable(happly' f g)
happly-lc fe f g = section-lc happly ((prโ‚‚ (fe f g)))

ap-funext : {X : ๐“ฅ ฬ‡ } {Y : ๐“ฆ ฬ‡} (f g : X โ†’ Y) {A : ๐“ฆ' ฬ‡} (k : Y โ†’ A) (h : f โˆผ g)
          โ†’ (fe : funext ๐“ฅ ๐“ฆ) (x : X) โ†’ ap (ฮป (- : X โ†’ Y) โ†’ k (- x)) (dfunext fe h) โ‰ก ap k (h x)
ap-funext f g k h fe x = ap (ฮป - โ†’ k (- x)) (dfunext fe h)    โ‰กโŸจ refl โŸฉ
                         ap (k โˆ˜ (ฮป - โ†’ - x)) (dfunext fe h)  โ‰กโŸจ (ap-ap (ฮป - โ†’ - x) k (dfunext fe h))โปยน โŸฉ
                         ap k (ap (ฮป - โ†’ - x) (dfunext fe h)) โ‰กโŸจ refl โŸฉ
                         ap k (happly (dfunext fe h) x)       โ‰กโŸจ ap (ฮป - โ†’ ap k (- x)) (happly-funext fe f g h) โŸฉ
                         ap k (h x) โˆŽ

\end{code}

The following is taken from this thread:
https://groups.google.com/forum/#!msg/homotopytypetheory/VaLJM7S4d18/Lezr_ZhJl6UJ

\begin{code}

transport-funext : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) (P : (x : X) โ†’ A x โ†’ ๐“ฆ ฬ‡) (fe : funext ๐“ค ๐“ฅ)
                   (f g : ฮ  A)
                   (ฯ† : (x : X) โ†’ P x (f x))
                   (h : f โˆผ g)
                   (x : X)
                 โ†’ transport (ฮป - โ†’ (x : X) โ†’ P x (- x)) (dfunext fe h) ฯ† x
                 โ‰ก transport (P x) (h x) (ฯ† x)
transport-funext A P fe f g ฯ† h x = q โˆ™ r
 where
  l : (f g : ฮ  A) (ฯ† : โˆ€ x โ†’ P x (f x)) (p : f โ‰ก g)
        โ†’ โˆ€ x โ†’ transport (ฮป - โ†’ โˆ€ x โ†’ P x (- x)) p ฯ† x
              โ‰ก transport (P x) (happly p x) (ฯ† x)
  l f .f ฯ† refl x = refl

  q : transport (ฮป - โ†’ โˆ€ x โ†’ P x (- x)) (dfunext fe h) ฯ† x
    โ‰ก transport (P x) (happly (dfunext fe h) x) (ฯ† x)
  q = l f g ฯ† (dfunext fe h) x

  r : transport (P x) (happly (dfunext fe h) x) (ฯ† x)
    โ‰ก transport (P x) (h x) (ฯ† x)
  r = ap (ฮป - โ†’ transport (P x) (- x) (ฯ† x)) (happly-funext fe f g h)

\end{code}