<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">For those who don't speak Agda, I think the idea is this (Alan, please correct me if I'm wrong): <div><br></div><div>(a) Postulate a map</div><div><br></div><div>ua : A ≃ B -> A = B</div><div><br></div><div>where for (e : A ≃ B), if </div><div>(1) A is definitionally equal to B</div><div>(2) e is definitionally equal to the identity equivalence</div><div>then ua e is definitionally equal to refl</div><div><br></div><div>(i.e. ua (id-equiv) is definitionally refl). </div><div><br></div><div>(b) Postulate</div><div><br></div><div>ua-beta : for all (e : A ≃ B), idtoeqv (ua e) = e</div><div><br></div><div>such that under (1) and (2) as in (a), </div><div>ua-beta e is definitionally equal to refl.</div><div><br></div><div>(c) From this, it follows that </div><div><br></div><div>ua-eta : for all (p : A = B), ua(idtoeqv p) = p</div><div><br></div><div>(Do path induction on p, and idtoeqv refl is the identity equivalence, so (1) and (2) hold, so ua (idtoeqv refl) is refl.)</div><div><br></div><div>(d) Similarly, the fifth component of the adjoint equivalence is path induction followed by reflexivity.</div><div><br></div><div>Does univalence preserve the identity strictly in any of the models?</div><div><br></div><div>-Dan</div><div><br></div><div><br><div><div>On Jan 17, 2015, at 8:11 AM, Jason Gross <<a href="mailto:jasongross9@gmail.com">jasongross9@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><p dir="ltr">I'm cc'ing the homotopy type theory list as well.</p><p dir="ltr">To answer some of your questions:<br>
(a) I've not seen this before. It seems pretty neat!<br>
(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.</p><p dir="ltr">-Jason</p>
<div class="gmail_quote">On Jan 17, 2015 2:33 AM, "Alan Jeffrey" <<a href="mailto:ajeffrey@bell-labs.com">ajeffrey@bell-labs.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi everyone,<br>
<br>
In the Agda development of Homotopy Type Theory at <a href="https://github.com/HoTT/HoTT-Agda/" target="_blank">https://github.com/HoTT/HoTT-<u></u>Agda/</a> the univalence axiom is given by three postulates (the map from (A ≃ B) to (A ≡ B) and its β and η rules).<br>
<br>
I wonder whether these postulates could be replaced by uses of primTrustMe?<br>
<br>
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:<br>
<br>
primTrustMe M M → refl<br>
<br>
In the attached Agda code, primTrustMe is used to define:<br>
<br>
private<br>
trustme : ∀ {ℓ} {A B : Set ℓ} (p : A ≃ B) → (∃ q ∙ ((≡-to-≃ q) ≡ p))<br>
trustme p = ⟨ primTrustMe , primTrustMe ⟩<br>
<br>
from which we get the map from (A ≃ B) to (A ≡ B) and its β rule:<br>
<br>
≃-to-≡ : ∀ {ℓ} {A B : Set ℓ} → (A ≃ B) → (A ≡ B)<br>
≃-to-≡ p with trustme p<br>
≃-to-≡ .(≡-to-≃ refl) | ⟨ refl , refl ⟩ = refl<br>
<br>
≃-to-≡-β : ∀ {ℓ} {A B : Set ℓ} (p : A ≃ B) → (≡-to-≃ (≃-to-≡ p) ≡ p)<br>
≃-to-≡-β p with trustme p<br>
≃-to-≡-β .(≡-to-≃ refl) | ⟨ refl , refl ⟩ = refl<br>
<br>
Interestingly, the η rule and the coherence property for β and η then become trivial:<br>
<br>
≃-to-≡-η : ∀ {ℓ} {A B : Set ℓ} (p : A ≡ B) → (≃-to-≡ (≡-to-≃ p) ≡ p)<br>
≃-to-≡-η refl = refl<br>
<br>
≃-to-≡-τ : ∀ {ℓ} {A B : Set ℓ} (p : A ≡ B) →<br>
(cong ≡-to-≃ (≃-to-≡-η p) ≡ ≃-to-≡-β (≡-to-≃ p))<br>
≃-to-≡-τ refl = refl<br>
<br>
Note there's some hoop-jumping with private declarations to hide trustme from users, because:<br>
<br>
(fst (trustme p)) → refl (for any p : (A ≃ A))<br>
<br>
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).<br>
<br>
Now, this isn't a conservative extension of HOTT because it introduces extra beta reductions that were previously just propositional equalities, in particular:<br>
<br>
(≃-to-≡ (≡-to-≃ refl)) → refl<br>
(≃-to-≡-β (≡-to-≃ refl)) → refl<br>
(≃-to-≡-η refl) → refl<br>
(≃-to-≡-τ refl) → refl<br>
<br>
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?<br>
<br>
Alan.<br>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><div><br class="webkit-block-placeholder"></div>
-- <br>
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.<br>
To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br>
For more options, visit <a href="https://groups.google.com/d/optout">https://groups.google.com/d/optout</a>.<br>
</blockquote></div><br></div></body></html>