[Agda] Univalence via Agda's primTrustMe?
Jason Gross
jasongross9 at gmail.com
Sun Jan 18 03:40:39 CET 2015
On Sun, Jan 18, 2015 at 12:18 AM, Alan Jeffrey <ajeffrey at bell-labs.com>
wrote:
> Thanks! Are there good "victory conditions" for a computational
> interpretation of univalence? Other than "I know it when I see it" :-)
>
If every function defined by pattern matching on a path
reduces judgmentally when applied to univalence (i.e., if the strong normal
form of a term contains no pattern matching on univalence), then we've
won. I don't know anything better than that.
-Jason
>
> A.
>
> On 01/17/2015 07:11 AM, Jason Gross wrote:
>
>> I'm cc'ing the homotopy type theory list as well.
>>
>> To answer some of your questions:
>> (a) I've not seen this before. It seems pretty neat!
>> (c) This is, in some sense, the simplest part of computational
>> univalence. All of the thoughts I've had about computational univalence
>> go top down, saying what should happen when you do path induction on an
>> equality from univalence. But it's cool to see what you can do bottom-up.
>>
>> -Jason
>>
>> On Jan 17, 2015 2:33 AM, "Alan Jeffrey" <ajeffrey at bell-labs.com
>> <mailto:ajeffrey at bell-labs.com>> wrote:
>>
>> Hi everyone,
>>
>> In the Agda development of Homotopy Type Theory at
>> https://github.com/HoTT/HoTT-__Agda/
>>
>> <https://github.com/HoTT/HoTT-Agda/> the univalence axiom is given
>> by three postulates (the map from (A ≃ B) to (A ≡ B) and its β and η
>> rules).
>>
>> I wonder whether these postulates could be replaced by uses of
>> primTrustMe?
>>
>> As a reminder, primTrustMe is a trusted function which inhabits the
>> type (M ≡ N) for any M and N. It is possible to introduce
>> contradictions (e.g. 0 ≡ 1) in the same way as with postulates, so
>> it has to be handled with care. The semantics is as for postulates,
>> but with an extra beta reduction:
>>
>> primTrustMe M M → refl
>>
>> In the attached Agda code, primTrustMe is used to define:
>>
>> private
>> trustme : ∀ {ℓ} {A B : Set ℓ} (p : A ≃ B) → (∃ q ∙ ((≡-to-≃ q)
>> ≡ p))
>> trustme p = ⟨ primTrustMe , primTrustMe ⟩
>>
>> from which we get the map from (A ≃ B) to (A ≡ B) and its β rule:
>>
>> ≃-to-≡ : ∀ {ℓ} {A B : Set ℓ} → (A ≃ B) → (A ≡ B)
>> ≃-to-≡ p with trustme p
>> ≃-to-≡ .(≡-to-≃ refl) | ⟨ refl , refl ⟩ = refl
>>
>> ≃-to-≡-β : ∀ {ℓ} {A B : Set ℓ} (p : A ≃ B) → (≡-to-≃ (≃-to-≡ p) ≡
>> p)
>> ≃-to-≡-β p with trustme p
>> ≃-to-≡-β .(≡-to-≃ refl) | ⟨ refl , refl ⟩ = refl
>>
>> Interestingly, the η rule and the coherence property for β and η
>> then become trivial:
>>
>> ≃-to-≡-η : ∀ {ℓ} {A B : Set ℓ} (p : A ≡ B) → (≃-to-≡ (≡-to-≃ p) ≡
>> p)
>> ≃-to-≡-η refl = refl
>>
>> ≃-to-≡-τ : ∀ {ℓ} {A B : Set ℓ} (p : A ≡ B) →
>> (cong ≡-to-≃ (≃-to-≡-η p) ≡ ≃-to-≡-β (≡-to-≃ p))
>> ≃-to-≡-τ refl = refl
>>
>> Note there's some hoop-jumping with private declarations to hide
>> trustme from users, because:
>>
>> (fst (trustme p)) → refl (for any p : (A ≃ A))
>>
>> that is, all proofs of (A ≃ A) would be identified if we were
>> allowed unfettered access to trustme. Instead, we only allow (≃-to-≡
>> p) to reduce to refl when (trustme p) reduces to ⟨ refl , refl ⟩,
>> that is not only do we have (A ≃ A) but also that p must be the
>> trivial proof that (A ≃ A).
>>
>> Now, this isn't a conservative extension of HOTT because it
>> introduces extra beta reductions that were previously just
>> propositional equalities, in particular:
>>
>> (≃-to-≡ (≡-to-≃ refl)) → refl
>> (≃-to-≡-β (≡-to-≃ refl)) → refl
>> (≃-to-≡-η refl) → refl
>> (≃-to-≡-τ refl) → refl
>>
>> So questions... a) Is this re-inventing the wheel? b) Is this sound?
>> c) Is there a connection between this and a computational
>> interpretation of univalence?
>>
>> Alan.
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150118/5a7627f2/attachment-0001.html
More information about the Agda
mailing list