FUNCTION EXTENSIONALITY

Here is presented two packages of homotopy, denoted as , between two functions from function space. The first is isomorphism structure with as encode-decode functions and as section-retract properties; and the second is identity system structure with as reflection and as induction principle.

Formation

(Homotopy Formation). Homotopy is the equality of functions .

def ~ (A B: U) (f g: A -> B)
  : U := Path (A -> B) f g

Introduction

(Homotopy Introduction, Function Extensionality).

def funext (A B: U) (f g: A → B)
    (p: Π (x: A), Path B (f x) (g x))
  : ~ A B f g
 := <i> λ (a: A), p a @ i

(Homotopy Dependent Introduction).

def piext (A: U) (B: A -> U) (f g: (x: A) -> B x)
    (p: (x: A) -> Path (B x) (f x) (g x))
  : Path ((y: A) -> B y) f g
 := <i> λ (a: A), p a @ i

(Homotopy Reflection).

def funext-id (A: U)
  : ~ A A (id A) (id A)
 := <_> id A

Elimination

(Homotopy Elimination).

def happly (A B: U) (f g: A -> B)
    (p: Path (A -> B) f g) (x: A)
  : Path B (f x) (g x)
 := cong (A → B) B
         (λ (h: A → B), app A B h x) f g p

(Homotopy Induction). For any and it's evidence at there is a function . HoTT 5.8.5

def funext-ind (A B: U) (f g: A → B) (C: funext-D A B)
    (d: Π (f g: A → B), C f f (<_>\(x:A), f x))
  : Π (h: Path (A → B) f g), C f g h
 := λ (h: Path (A → B) f g),
      subst (singl (A → B) f)
            (\ (z: singl (A → B) f), C f (z.1) (z.2))
            (eta (A → B) f)
            (g, h)
            (contr (A → B) f g h)
            (d f g)

Computation

(Homotopy Isomorphism Computation).

def funext-β (A B: U) (f g: A → B)
    (p: Π (x: A), Path B (f x) (g x))
  : Π (x: A), Path B (f x) (g x)
 := λ (x: A), happly A B f g (funext A B f g p) x

(Homotopy Induction Principle Computation).

def funext-ind-β (A B: U) (f g : A → B) (C : funext-D A B)
    (d: Π (f g: A → B), C f f (<_>\(x:A), f x))
  : Path (C f f (<_>f)) (d f f) (funext-ind A B f f C d (<_>f))
 := subst-comp (singl (A → B) f)
               (\ (z: singl (A → B) f), C f (z.1) (z.2))
               (eta (A → B) f)
               (d f f)

Uniqueness

(Homotopy Isomorphism Uniqueness).

def funext-η (A B: U) (f g: A → B)
    (p: Path (A → B) f g)
  : Path (Path (A → B) f g)
         (funext A B f g (happly A B f g p)) p
 := idp (Path (A → B) f g) p