FUNEXT

# 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