Function Extensionality
Table of Contents
1 Function extensionality
module Lib.FunExt where
This file defines function extensionnality and provides the bijection between the two ways.
1.1 Packages imports
The imported packages can be accessed via the following links:
import Stdlib.Prelude import Lib.Data.QInv
1.2 Definitions
First, we define eq-htpy and htpy-eq that should be inverses.
eq-htpy (A : U) (B : A → U) (f g : (x : A) → B x) (H : Htpy A B f g) : Path ((x : A) → B x) f g = λi a. H a i htpy-eq (A : U) (B : A → U) (f g : (x : A) → B x) (p : Path ((x : A) → B x) f g) : Htpy A B f g = λx i. p i x eq-htpy' (A B : U) (f g : A → B) (H : Htpy' A B f g) : Path (A → B) f g = eq-htpy A (λ_. B) f g H htpy-eq' (A B : U) (f g : A → B) (p : Path (A → B) f g) : Htpy' A B f g = htpy-eq A (λ_. B) f g p
1.3 Equivalence
The function extensionnality principle states that htpy-eq is a family of equivalences.
The right homotopy is reflexivity by definition.
htpy-eq/right-htpy (A : U) (B : A → U) (f g : (x : A) → B x) : Htpy' (Htpy A B f g) (Htpy A B f g) (λH. htpy-eq A B f g (eq-htpy A B f g H)) (id (Htpy A B f g)) = λH. refl (Htpy A B f g) (λx i. H x i)
The left homotopy is also reflexivity.
htpy-eq/left-htpy (A : U) (B : A → U) (f g : (x : A) → B x) : Htpy' (Path ((x : A) → B x) f g) (Path ((x : A) → B x) f g) (λp. eq-htpy A B f g (htpy-eq A B f g p)) (id (Path ((x : A) → B x) f g)) = λp. refl (Path ((x : A) → B x) f g) (λi a. p i a)
Thus, htpy-eq has an inverse.
htpy-eq/has-inverse (A : U) (B : A → U) (f g : (x : A) → B x) : has-inverse (Path ((x : A) → B x) f g) (Htpy A B f g) (htpy-eq A B f g) = (eq-htpy A B f g, (htpy-eq/right-htpy A B f g, htpy-eq/left-htpy A B f g))
Same for eq-htpy.
eq-htpy/has-inverse (A : U) (B : A → U) (f g : (x : A) → B x) : has-inverse (Htpy A B f g) (Path ((x : A) → B x) f g) (eq-htpy A B f g) = (htpy-eq A B f g, (htpy-eq/left-htpy A B f g, htpy-eq/right-htpy A B f g))