Incorporate reverse-ap for proving equivalence #1
Labels
No labels
asking-favonia
exercise
questions
size
L
T-equivalence
No milestone
No project
No assignees
1 participant
Notifications
Total time spent: 59 minutes 21 seconds
Due date
michael
59 minutes 21 seconds
No due date set.
Dependencies
No dependencies set.
Reference: michael/type-theory#1
Loading…
Reference in a new issue
No description provided.
Delete branch "%!s()"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
The bool equiv problem requires us to give an equivalence between fibers. For two fibers
r = (x, f x ≡ y)
andr' = (x', f x' ≡ y)
, we need to compare point-wise (x against x'), and (f x ≡ y against f x' ≡ y). In my terminology,r
is the "center" fiber of all the contractible fibers, andr'
is the for-all other fibers that are being compared.The crux of this proof comes from the fact that we can set both sides equal to
y
. When we havep1 = f x ≡ y
andp2 = f x' ≡ y
we can dof x ≡ f x'
. The tricky step here is that in order to turn this intox ≡ x'
, we have toap
the inverse of f.Normally you can't just "un-
ap
" a function but since we know we are working with equivalences we can get the inverse with the functionf-inv y = x
. But I don't think this actually works because this doesn't actually generalize automatically yet? Pending more investigationOk I think I had a slight breakthrough with why I was getting this wrong. I had thought that for a function (f : A -> B) and particular (y : B), the fiber would be (y, f x ≡ y) because of the notation that I used, but this makes no sense: the y is already fixed.
The fiber is actually the (x : A), along with the f x ≡ y.
Ok Favonia's hint is to compute "ap g p", and then concatenate it with a proof that g is the left-inverse of f
Trying with:
This isn't accepting the first question mark there, even though I've defined:
I think I got the idea, see this file
I got by with proving:
and then just applying this works