[HoTT] Re: [Agda] Univalence via Agda's primTrustMe?

[Alan Jeffrey]

Yes, that is a good non-Agda summary. I think it's interesting that this 
can be expressed in Agda without modification (but by using a 
potentially unsound feature).

A.

On 01/17/2015 10:56 AM, Dan Licata wrote:
> For those who don't speak Agda, I think the idea is this (Alan, please
> correct me if I'm wrong):
>
> (a) Postulate a map
>
> ua : A ≃ B -> A = B
>
> where for (e : A ≃ B), if
> (1) A is definitionally equal to B
> (2) e is definitionally equal to the identity equivalence
> then ua e is definitionally equal to refl
>
> (i.e. ua (id-equiv) is definitionally refl).
>
> (b) Postulate
>
> ua-beta : for all (e : A ≃ B), idtoeqv (ua e) = e
>
> such that under (1) and (2) as in (a),
> ua-beta e is definitionally equal to refl.
>
> (c) From this, it follows that
>
> ua-eta : for all (p : A = B), ua(idtoeqv p) = p
>
> (Do path induction on p, and idtoeqv refl is the identity equivalence,
> so (1) and (2) hold, so ua (idtoeqv refl) is refl.)
>
> (d) Similarly, the fifth component of the adjoint equivalence is path
> induction followed by reflexivity.
>
> Does univalence preserve the identity strictly in any of the models?
>
> -Dan
>
>
> On Jan 17, 2015, at 8:11 AM, Jason Gross <jasongross9 at gmail.com
> <mailto:jasongross9 at gmail.com>> 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
>>
>>
>> --
>> You received this message because you are subscribed to the Google
>> Groups "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send
>> an email to HomotopyTypeTheory+unsubscribe at googlegroups.com
>> <mailto:HomotopyTypeTheory+unsubscribe at googlegroups.com>.
>> For more options, visit https://groups.google.com/d/optout.
>