Quest 4 - Side Quests

Functional Extensionality

We show that two dependent functions f g being equal is the same as them being equal when applied to each value of the domain. We call one of these directions functional extensionality :

funExt : {B : A → Type} {f g : (a : A) → B a} →
   ((a : A) → f a ≡ g a) → f ≡ g
funExt = {!!}

Write this up in agda and have a go at it.

We will cheat and use the native cubical definition of paths (rather than using our axiomatic approach with J and JRefl etc), since the HoTT proof of this is much more work. A path in cubical agda between two points x and y in a space A can be defined by just taking an arbitrary point i on the “interval” I, to a point in the space A, such that the end points agree. Assuming we have the bundle B, functions f g, a proof h of (a : A) → f a ≡ ga, we can refine, and agda will assume such an i for us.

funExt : {B : A → Type} {f g : (a : A) → B a} →
  ((a : A) → f a ≡ g a) → f ≡ g
funExt h = λ i a → {!!}

Checking the goal you should see something like the following (we have extracted the important parts):

  Goal: B a
——————————————————————————————————
a : A
i : I
h : (a₁ : A) → f a₁ ≡ g a₁
g : (a₁ : A) → B a₁   (not in scope)
f : (a₁ : A) → B a₁   (not in scope)
B : A → Type   (not in scope)
A : Type   (not in scope)
———— Constraints ————————————————————————
?0 (i = i1) = g a : B a
?0 (i = i0) = f a : B a

We break this down :

• agda has assumed an arbitrary i : I and a : A, and is now asking for a point in B a.

• Let’s call whatever we put in the goal ?0; it has type B a. The constraints say that at the start and end points of I (called i0 and i1 respectively) 0? i should be f a and g a respectively.

• To understand why agda also gave us an a : A we can go back a step, removing a. You should see that the goal at that point was a dependent function that at the start and end points are f and g respectively.

• Try to complete the quest. You will need that given a path p and i : I along the interval, writing p i gives the corresponding point along the path p.

Hint

The hypothesis h applied to the point a gives us a path from f a to g a in B a.

Solution

funExt : {B : A → Type} {f g : (a : A) → B a} →
  ((a : A) → f a ≡ g a) → f ≡ g
funExt h = λ i a → h a i

Now we can promote this to an isomorphism, hence an equality between f ≡ g and (a : A) → f a ≡ g a. Try to formalize and prove this.

Solution

funExtPath : (B : A → Type) (f g : (a : A) → B a) → (f ≡ g) ≡ ((a : A) → f a ≡ g a) funExtPath {A} B f g = isoToPath (iso fun (funExt B f g) rightInv leftInv) where

fun : f ≡ g → (a : A) → f a ≡ g a fun h = λ a i → h i a

rightInv : section fun (funExt B f g) rightInv h = refl

leftInv : retract fun (funExt B f g) leftInv h = refl

Justifying J

Work in progress.