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 --exact-split #-}

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 = (๐ค ๐ฅ : 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 : {๐ค ๐ฅ : Universe}
{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:

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

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}