Function extensionality is not derivable in Agda or Coq. It can be postulated as an axiom that is consistent with the theory, but you cannot construct a term for the type representing function extensionality.

In Cubical Agda it is derivable and it has a tauntingly concise definition. (removing Level for a moment since that is tangental)

```
funext : {A B : Set}{f g : A → B} → (∀ (a : A) → f a ≡ g a) → f ≡ g
funext p i a = p a i
```

That said, there is a fair amount to unpack to understand what is going on here.

Cubical Agda adds an abstract Interval Type `I`

which has two endpoints `i0`

and `i1`

. (see footnote [1])

Equality in Cubical Agda is represented by Path Types.

```
_≡_ : {A : Set} -> A -> A -> Set
_≡_ {A} x y = Path A x y
```

read as … `x`

and `y`

are equal elements of `A`

when there is a `Path`

in `A`

from `x`

to `y`

. A Path is constructed by abstracting over an abstract interval `I`

and saying where each endpoint (`i0`

and `i1`

) maps to. (subject to some constraints) Here is a concrete example.

```
data Bool : Set where
true : Bool
false : Bool
true-eq-true : Path Bool true true
true-eq-true = λ i -> true
```

This says we have a `Path`

in `Bool`

between elements `true`

and `true`

(Aka `true ≡ true`

).

We construct this path by abstracting over an interval `i`

and setting both endpoints `i0`

and `i1`

to `true`

.

Paths can be sampled at their endpoints using a syntax similar to function application.

for instance given `p : a ≡ b`

.

I can sample the left endpoint by applying `p`

to `i0`

so `p i0 := a`

I can sample the right endpoint by applying `p`

to `i1`

so `p i1 := b`

Now back to funext

```
funext : {A B : Set}{f g : A → B} → (∀ (a : A) → f a ≡ g a) → f ≡ g
funext = ?
```

First take in the argument `p`

of type `(∀ (a : A) → f a ≡ g a) `

from the hypothesis.

```
funext : {A B : Set}{f g : A → B} → (∀ (a : A) → f a ≡ g a) → f ≡ g
funext p = ?
```

then the goal is `f ≡ g`

.

We have to construct a Path (in `A -> B`

)from `f`

to `g`

, so we have to abstract over an inverval `i : I`

```
funext : {A B : Set}{f g : A → B} → (∀ (a : A) → f a ≡ g a) → f ≡ g
funext p i = ?
```

Since we are defining a path in the function space `A -> B`

, the endpoints `i0`

and `i1`

each need to map to something of type `A -> B`

. So we can start by abstracting over `a : A`

```
funext : {A B : Set}{f g : A → B} → (∀ (a : A) → f a ≡ g a) → f ≡ g
funext p i a = ?
```

Our goal is now to construct an element of `B`

.

Using `p : ∀ (a : A) → f a ≡ g a) `

and `a : A`

we can get a path `f a ≡ g a`

.

`p a : f a ≡ g a`

is a path from `f a`

to `g a`

both of which have type `B`

.

Paths can be sampled at their endpoints so we apply `p a`

to `i`

and get an element of `B`

```
funext : {A B : Set}{f g : A → B} → (∀ (a : A) → f a ≡ g a) → f ≡ g
funext p i a = p a i
```

To see what is happening here let’s consider what happens at each endpoint of the interval.

When `i := i0`

, `p a i0 := f a`

when `i := i1`

, `p a i1 := g a`

Foot notes: [1]

Cubical agda internalizes the higher inductive type `I`

into the type theory.

```
data I : Set where
i0 : I
i1 : I
eq : i0 ≡ i1
```

So the `eq`

condition must be obeyed when constructing paths that is to say that the endpoints must be definitionally equal.

more details can be found here: https://agda.readthedocs.io/en/v2.6.2.1/language/cubical.html