[Agda] Univalence via Agda's primTrustMe?

[Alan Jeffrey]

Hi Andy,

In fairness to Agda, primTrustMe (and the other primitives) are intended 
for the authors of data types using the FFI to provide Agda language 
bindings for the compiler back ends. The poster child for primTrustMe is 
equality on unicode strings, which you really don't want to have to do 
by hand, so has a primitive:

   primStringEquality : String -> String -> Bool

You'd like to be able to use this string equality in proofs, which is 
where primTrustMe comes in:

   _=?=_ : (x y : String) -> Dec(x == y)
   x =?= y with primStringEquality x y
   ... | true = yes primTrustMe
   ... | false = no x<>y where postulate x<>y : _

The function primTrustMe is only really intended for use by writers of 
FFI libraries for primitive types, so it's not too surprising that the 
documentation is, er, sparse. It was never intended for things like 
defining univalence.

A.

On 01/17/2015 11:52 AM, Andrew Pitts wrote:
> 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.