<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Jan 18, 2015 at 12:18 AM, Alan Jeffrey <span dir="ltr"><<a href="mailto:ajeffrey@bell-labs.com" target="_blank" onclick="window.open('https://mail.google.com/mail/?view=cm&tf=1&to=ajeffrey@bell-labs.com&cc=&bcc=&su=&body=','_blank');return false;">ajeffrey@bell-labs.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">Thanks! Are there good "victory conditions" for a computational interpretation of univalence? Other than "I know it when I see it" :-)<br></blockquote><div><br></div><div>If every function defined by pattern matching on a path reduces judgmentally when applied to univalence (i.e., if the strong normal form of a term contains no pattern matching on univalence), then we've won. I don't know anything better than that.</div><div><br></div><div>-Jason</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<br>
A.<span class=""><br>
<br>
On 01/17/2015 07:11 AM, Jason Gross wrote:<br>
</span><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><span class="">
I'm cc'ing the homotopy type theory list as well.<br>
<br>
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<br>
univalence. All of the thoughts I've had about computational univalence<br>
go top down, saying what should happen when you do path induction on an<br>
equality from univalence. But it's cool to see what you can do bottom-up.<br>
<br>
-Jason<br>
<br>
On Jan 17, 2015 2:33 AM, "Alan Jeffrey" <<a href="mailto:ajeffrey@bell-labs.com" target="_blank" onclick="window.open('https://mail.google.com/mail/?view=cm&tf=1&to=ajeffrey@bell-labs.com&cc=&bcc=&su=&body=','_blank');return false;">ajeffrey@bell-labs.com</a><br></span><span class="">
<mailto:<a href="mailto:ajeffrey@bell-labs.com" target="_blank" onclick="window.open('https://mail.google.com/mail/?view=cm&tf=1&to=ajeffrey@bell-labs.com&cc=&bcc=&su=&body=','_blank');return false;">ajeffrey@bell-labs.com</a><u></u>>> wrote:<br>
<br>
Hi everyone,<br>
<br>
In the Agda development of Homotopy Type Theory at<br></span>
<a href="https://github.com/HoTT/HoTT-__Agda/" target="_blank">https://github.com/HoTT/HoTT-_<u></u>_Agda/</a><div><div class="h5"><br>
<<a href="https://github.com/HoTT/HoTT-Agda/" target="_blank">https://github.com/HoTT/HoTT-<u></u>Agda/</a>> the univalence axiom is given<br>
by three postulates (the map from (A ≃ B) to (A ≡ B) and its β and η<br>
rules).<br>
<br>
I wonder whether these postulates could be replaced by uses of<br>
primTrustMe?<br>
<br>
As a reminder, primTrustMe is a trusted function which inhabits the<br>
type (M ≡ N) for any M and N. It is possible to introduce<br>
contradictions (e.g. 0 ≡ 1) in the same way as with postulates, so<br>
it has to be handled with care. The semantics is as for postulates,<br>
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)<br>
≡ 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 η<br>
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<br>
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<br>
allowed unfettered access to trustme. Instead, we only allow (≃-to-≡<br>
p) to reduce to refl when (trustme p) reduces to ⟨ refl , refl ⟩,<br>
that is not only do we have (A ≃ A) but also that p must be the<br>
trivial proof that (A ≃ A).<br>
<br>
Now, this isn't a conservative extension of HOTT because it<br>
introduces extra beta reductions that were previously just<br>
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?<br>
c) Is there a connection between this and a computational<br>
interpretation of univalence?<br>
<br>
Alan.<br>
<br>
______________________________<u></u>_________________<br>
Agda mailing list<br></div></div>
<a href="mailto:Agda@lists.chalmers.se" target="_blank" onclick="window.open('https://mail.google.com/mail/?view=cm&tf=1&to=Agda@lists.chalmers.se&cc=&bcc=&su=&body=','_blank');return false;">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank" onclick="window.open('https://mail.google.com/mail/?view=cm&tf=1&to=Agda@lists.chalmers.se&cc=&bcc=&su=&body=','_blank');return false;">Agda@lists.chalmers.se</a><u></u>><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br>
</blockquote>
</blockquote></div><br></div></div>