[Agda] Univalence via Agda's primTrustMe?

[Alan Jeffrey]

Thanks! Are there good "victory conditions" for a computational 
interpretation of univalence? Other than "I know it when I see it" :-)

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
>