![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
(no subject)
Jul. 17th, 2017 05:49 pmOn a train to pittsburgh.
My self-imposed agda-exercise for the train trip was to prove that assuming polymorphic functions
f : {C : Set} → (A → C) → (B → C) have the free theorem you expect them to from parametricity (namely (g : A → C1) (k : C1 → C2) → k ∘ (f g) == f (k ∘ g)) then
((C : Set) → (A → C) ≃ (B → C)) ≃ (B ≃ A)
Interestingly, it was very easy to show
((C : Set) → (A → C) → (B → C)) ≃ (B → A)
and only mildly more challenging to show
((C : Set) → (A → C) ≃ (B → C)) → (B ≃ A)
but the equivalence-of-equivalences was pretty tricky. I succeeded with a few hours to spare, though! I did it by separating out the functions from the is-equiv property they satisfied, and taking advantage of the mere-proposition-ness of is-equiv.
Huh, and I didn't even need univalence, it looks like. Except for using function extensionality all over the place --- but as we all learned in HoTT kindergarten, that follows from the existence of an interval type also.
My self-imposed agda-exercise for the train trip was to prove that assuming polymorphic functions
f : {C : Set} → (A → C) → (B → C) have the free theorem you expect them to from parametricity (namely (g : A → C1) (k : C1 → C2) → k ∘ (f g) == f (k ∘ g)) then
Interestingly, it was very easy to show
and only mildly more challenging to show
but the equivalence-of-equivalences was pretty tricky. I succeeded with a few hours to spare, though! I did it by separating out the functions from the is-equiv property they satisfied, and taking advantage of the mere-proposition-ness of is-equiv.
Huh, and I didn't even need univalence, it looks like. Except for using function extensionality all over the place --- but as we all learned in HoTT kindergarten, that follows from the existence of an interval type also.
