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