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 --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 ๐ค ๐ฅ

Fun-Ext : ๐คฯ
Fun-Ext = {๐ค ๐ฅ : 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

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

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)  โกโจ (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:

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