[Agda] Univalence via Agda's primTrustMe?

[Jason Gross]

By the way, I've made a feature request for Coq to have something like
this, but more powerful: https://coq.inria.fr/bugs/show_bug.cgi?id=3927.
Perhaps Agda could use a similar extension?

On Sat, Jan 17, 2015 at 12:09 PM, Jason Gross <jasongross9 at gmail.com> wrote:

> Is it possible to push this even further?  For example, define an
> alternate definition of, say, ap, relying on primTrustMe in some fancy way
> such that when it gets either univalence or refl, it computes?
>
> -Jason
>
> On Sat, Jan 17, 2015 at 2:33 AM, Alan Jeffrey <ajeffrey at bell-labs.com>
> wrote:
>
>> Hi everyone,
>>
>> In the Agda development of Homotopy Type Theory at
>> 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
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150117/64fb7d46/attachment.html