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 arbitraryi : I
anda : A
, and is now asking for a point inB a
.Let’s call whatever we put in the goal
?0
; it has typeB a
. The constraints say that at the start and end points ofI
(calledi0
andi1
respectively)0? i
should bef a
andg a
respectively.To understand why
agda
also gave us ana : A
we can go back a step, removinga
. You should see that the goal at that point was a dependent function that at the start and end points aref
andg
respectively.Try to complete the quest. You will need that given a path
p
andi : I
along the interval, writingp i
gives the corresponding point along the pathp
.
The hypothesis Hint
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.
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 = reflSolution
Justifying J
Work in progress.