# 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.