Martin Escardo.

Formulation of function extensionality. Notice that this file doesn't
postulate function extensionality. It only defines the concept, which
is used explicitly as a hypothesis each time it is needed.

\begin{code}

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

module UF.FunExt where

open import MLTT.Spartan
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โ‚€ = funext ๐“คโ‚€ ๐“คโ‚€

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

Fun-Ext : ๐“คฯ‰
Fun-Ext = {๐“ค ๐“ฅ : Universe} โ†’ funext ๐“ค ๐“ฅ

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

abstract
 dfunext : funext ๐“ค ๐“ฅ โ†’ DN-funext ๐“ค ๐“ฅ
 dfunext fe {X} {A} {f} {g} = inverse (happly' f g) (fe f g)

 happly-funext : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ }
                 (fe : funext ๐“ค ๐“ฅ) (f g : ฮ  A) (h : f โˆผ g)
               โ†’ happly (dfunext fe h) ๏ผ h
 happly-funext fe f g = inverses-are-sections happly (fe f g)

 funext-happly : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ } (fe : funext ๐“ค ๐“ฅ)
               โ†’ (f g : ฮ  A) (h : f ๏ผ g)
               โ†’ dfunext fe (happly h) ๏ผ h
 funext-happly fe f g refl = inverses-are-retractions happly (fe f f) refl

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

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 (equivs-are-sections happly (fe f g))

inverse-happly-is-dfunext : {A : ๐“ค ฬ‡ } {B : ๐“ฅ ฬ‡ }
                            (feโ‚€ : funext ๐“ค ๐“ฅ)
                            (feโ‚ : funext (๐“ค โŠ” ๐“ฅ) (๐“ค โŠ” ๐“ฅ))
                            (f g : A โ†’ B)
                          โ†’ inverse (happly' f g) (feโ‚€ f g) ๏ผ dfunext feโ‚€
inverse-happly-is-dfunext feโ‚€ feโ‚ f g =
 dfunext feโ‚
  (ฮป h โ†’ happly-lc feโ‚€ f g
          (happly' f g (inverse (happly' f g) (feโ‚€ f g) h)
                                       ๏ผโŸจ inverses-are-sections _ (feโ‚€ f g) h โŸฉ
           h                           ๏ผโŸจ happly-funext feโ‚€ f g h โปยน โŸฉ
           happly' f g (dfunext feโ‚€ h) โˆŽ))

dfunext-refl : {X : ๐“ค ฬ‡ } {A : X โ†’ ๐“ฅ ฬ‡ }
               (fe : funext ๐“ค ๐“ฅ)
               (f : ฮ  A)
             โ†’ dfunext fe (ฮป (x : X) โ†’ ๐“ป๐“ฎ๐’ป๐“ต (f x)) ๏ผ refl
dfunext-refl fe f = happly-lc fe f f (happly-funext fe f f (ฮป x โ†’ refl))

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)  ๏ผโŸจ I โŸฉ
                         ap k (ap (ฮป - โ†’ - x) (dfunext fe h)) ๏ผโŸจ refl โŸฉ
                         ap k (happly (dfunext fe h) x)       ๏ผโŸจ II โŸฉ
                         ap k (h x)                           โˆŽ
                          where
                           I  = (ap-ap (ฮป - โ†’ - x) k (dfunext fe h))โปยน
                           II = ap (ฮป - โ†’ ap k (- x)) (happly-funext fe f g h)

ap-precomp-funext : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {A : ๐“ฆ ฬ‡ }
                    (f g : X โ†’ Y)
                    (k : A โ†’ X) (h : f โˆผ g)
                    (feโ‚€ : funext ๐“ค ๐“ฅ)
                    (feโ‚ : funext ๐“ฆ ๐“ฅ)
                  โ†’ ap (_โˆ˜ k) (dfunext feโ‚€ h) ๏ผ dfunext feโ‚ (h โˆ˜ k)
ap-precomp-funext f g k h feโ‚€ feโ‚ =
  ap (_โˆ˜ k) (dfunext feโ‚€ h)                        ๏ผโŸจ I โŸฉ
  dfunext feโ‚ (happly (ap (_โˆ˜ k) (dfunext feโ‚€ h))) ๏ผโŸจ II โŸฉ
  dfunext feโ‚ (h โˆ˜ k)                              โˆŽ
   where
    I  = funext-happly feโ‚ (f โˆ˜ k) (g โˆ˜ k) _ โปยน

    III = ฮป x โ†’
     ap (ฮป - โ†’ - x) (ap (_โˆ˜ k) (dfunext feโ‚€ h)) ๏ผโŸจ ap-ap _ _ (dfunext feโ‚€ h) โŸฉ
     ap (ฮป - โ†’ - (k x)) (dfunext feโ‚€ h)         ๏ผโŸจ ap-funext f g id h feโ‚€ (k x) โŸฉ
     ap (ฮป v โ†’ v) (h (k x))                     ๏ผโŸจ ap-id-is-id (h (k x)) โŸฉ
     h (k x)                                    โˆŽ

    II = ap (dfunext feโ‚) (dfunext feโ‚ III)

\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 =
 transport (ฮป - โ†’ โˆ€ x โ†’ P x (- x)) (dfunext fe h) ฯ† x ๏ผโŸจ I โŸฉ
 transport (P x) (happly (dfunext fe h) x) (ฯ† x)      ๏ผโŸจ II โŸฉ
 transport (P x) (h x) (ฯ† x) โˆŽ
 where
  lemma : (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)
  lemma f f ฯ† refl x = refl

  I  = lemma f g ฯ† (dfunext fe h) x
  II = ap (ฮป - โ†’ transport (P x) (- x) (ฯ† x)) (happly-funext fe f g h)

transport-funext' : {X : ๐“ค ฬ‡ } (A : ๐“ฅ ฬ‡ )
                    (P : X โ†’ A โ†’ ๐“ฆ ฬ‡ )
                    (fe : funext ๐“ค ๐“ฅ)
                    (f g : X โ†’ 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 = transport-funext (ฮป _ โ†’ A) P

\end{code}