[Agda] Univalence via Agda's primTrustMe?

[Andrew Pitts]

Alan's interesting post illustrates a difficulty faced by "ordinary
users" of Agda, such as me. Not having heard about primTrustMe, I
thought I would take a look at Alan's code to see how it can be used.
I see from his code that one can't just use primTrustMe without first
telling Agda that one wants to use it, via the "primitive" keyword.
Since I am not familiar with that, I looked up "primitive" in the
Reference Manual
<http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.TOC>....argh!
it is one of those annoying things coloured red in the table of
contents, meaning no info there yet.

Is there a description somewhere of all the existing primitives that
the current version of Agda knows about?

Agda is truly wonderful, but its documentation needs more work
(boring, but highly necessary). Is anyone working on an "Agda
documentation project"?

Andy Pitts

On 16 January 2015 at 21:03, 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.