<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): &nbsp;<div><br></div><div>(a) Postulate a map</div><div><br></div><div>ua : A ≃ B -&gt; A = B</div><div><br></div><div>where for (e :&nbsp;A ≃ B), if&nbsp;</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). &nbsp;</div><div><br></div><div>(b) Postulate</div><div><br></div><div>ua-beta : for all (e :&nbsp;A ≃ B), idtoeqv (ua e) = e</div><div><br></div><div>such that under (1) and (2) as in (a),&nbsp;</div><div>ua-beta e is definitionally equal to refl.</div><div><br></div><div>(c) From this, it follows that&nbsp;</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 &lt;<a href="mailto:jasongross9@gmail.com">jasongross9@gmail.com</a>&gt; 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.&nbsp; It seems pretty neat!<br>
(c) This is, in some sense, the simplest part of computational univalence.&nbsp; 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.&nbsp; 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" &lt;<a href="mailto:ajeffrey@bell-labs.com">ajeffrey@bell-labs.com</a>&gt; 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>
&nbsp; primTrustMe M M → refl<br>
<br>
In the attached Agda code, primTrustMe is used to define:<br>
<br>
&nbsp; private<br>
&nbsp; &nbsp; trustme : ∀ {ℓ} {A B : Set ℓ} (p : A ≃ B) → (∃ q ∙ ((≡-to-≃ q) ≡ p))<br>
&nbsp; &nbsp; trustme p = ⟨ primTrustMe , primTrustMe ⟩<br>
<br>
from which we get the map from (A ≃ B) to (A ≡ B) and its β rule:<br>
<br>
&nbsp; ≃-to-≡ : ∀ {ℓ} {A B : Set ℓ} → (A ≃ B) → (A ≡ B)<br>
&nbsp; ≃-to-≡ p with trustme p<br>
&nbsp; ≃-to-≡ .(≡-to-≃ refl) | ⟨ refl , refl ⟩ = refl<br>
<br>
&nbsp; ≃-to-≡-β : ∀ {ℓ} {A B : Set ℓ} (p : A ≃ B) → (≡-to-≃ (≃-to-≡ p) ≡ p)<br>
&nbsp; ≃-to-≡-β p with trustme p<br>
&nbsp; ≃-to-≡-β .(≡-to-≃ refl) | ⟨ refl , refl ⟩ = refl<br>
<br>
Interestingly, the η rule and the coherence property for β and η then become trivial:<br>
<br>
&nbsp; ≃-to-≡-η : ∀ {ℓ} {A B : Set ℓ} (p : A ≡ B) → (≃-to-≡ (≡-to-≃ p) ≡ p)<br>
&nbsp; ≃-to-≡-η refl = refl<br>
<br>
&nbsp; ≃-to-≡-τ : ∀ {ℓ} {A B : Set ℓ} (p : A ≡ B) →<br>
&nbsp; &nbsp; (cong ≡-to-≃ (≃-to-≡-η p) ≡ ≃-to-≡-β (≡-to-≃ p))<br>
&nbsp; ≃-to-≡-τ refl = refl<br>
<br>
Note there's some hoop-jumping with private declarations to hide trustme from users, because:<br>
<br>
&nbsp; (fst (trustme p)) → refl&nbsp; (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>
&nbsp; (≃-to-≡ (≡-to-≃ refl)) → refl<br>
&nbsp; (≃-to-≡-β (≡-to-≃ refl)) → refl<br>
&nbsp; (≃-to-≡-η refl) → refl<br>
&nbsp; (≃-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>