<div dir="ltr">Hi Dan,<div><br></div><div>Ah, thank you. That's very interesting.</div><div><br></div><div>Best,</div><div>Owen</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Oct 31, 2016 at 9:25 AM, Dan Licata <span dir="ltr"><<a href="mailto:drl@cs.cmu.edu" target="_blank">drl@cs.cmu.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Owen,<br>
<br>
I think AndEquals is the same as the Sigma/dependent pair type (p : Id A B) * Id{B} (coe p a) b that I was referring to (sorry for the confusion of using non-Agda notation).<br>
<span class="HOEnZb"><font color="#888888"><br>
-Dan<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
> On Oct 28, 2016, at 11:26 PM, Owen <<a href="mailto:ellbur@gmail.com">ellbur@gmail.com</a>> wrote:<br>
><br>
> Hi,<br>
><br>
> I should think for 2 minutes before I hit "send". Of course this works:<br>
><br>
> rewrite-type : (A : Set) (B : Set) (a : A) (eq : A ≡ B) → B<br>
> rewrite-type A .(A) a refl = a<br>
><br>
> data AndEquals : (A : Set) (B : Set) (a : A) (b : B) → Set₁ where<br>
> and-refl : {A : Set} {B : Set} {a : A} {b : B} (fst : A ≡ B) (snd : a ≡ (rewrite-type B A b (sym fst))) → AndEquals A B a b<br>
><br>
> I'm still curious whether this is substantially different than heterogeneous equality.<br>
><br>
> Best,<br>
> Owen<br>
><br>
> On Fri, Oct 28, 2016 at 11:21 PM, Owen <<a href="mailto:ellbur@gmail.com">ellbur@gmail.com</a>> wrote:<br>
> Hi,<br>
><br>
> I'm a complete beginner at Agda, so I tried to type in what I thought would be the "most natural" way to define an equality for vectors:<br>
><br>
> data AndEquals : (A : Set) (B : Set) (a : A) (b : B) → Set where<br>
> and-refl : {A : Set} {B : Set} {a : A} {b : B} (fst : A ≡ B) (snd : a ≡ b) → AndEquals A B a b<br>
><br>
> or, in words, "the types are equal and the terms are equal", where the "and" is a dependent "and" where the fact that the types are equal can be used to help express what is meant by "the terms are equal".<br>
><br>
> This definition of course fails to type-check because `a ≡ b` has operands of different types. If I could somehow rewrite the type of `b` to be `A` it could work.<br>
><br>
> Is the above definition substantially different than heterogeneous equality?<br>
><br>
> Does anyone have advice for how it could be made to type-check?<br>
><br>
> Best,<br>
> Owen<br>
><br>
> On Fri, Oct 28, 2016 at 10:23 PM, Dan Licata <<a href="mailto:drl@cs.cmu.edu">drl@cs.cmu.edu</a>> wrote:<br>
> Hi,<br>
><br>
> Here’s the thread I had in mind from a “few” years ago :)<br>
> <a href="https://lists.chalmers.se/pipermail/agda/2008/000153.html" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>pipermail/agda/2008/000153.<wbr>html</a><br>
> See in particular Conor’s reply here:<br>
> <a href="https://lists.chalmers.se/pipermail/agda/2008/000155.html" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>pipermail/agda/2008/000155.<wbr>html</a><br>
> and here:<br>
> <a href="https://lists.chalmers.se/pipermail/agda/2008/000159.html" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>pipermail/agda/2008/000159.<wbr>html</a><br>
><br>
> In current Agda (2.5.1.1), it looks like the existential interpretation is there: you can prove (even without K) by pattern matching that<br>
><br>
> data HId {A : Set} (M : A) : {B : Set} → B → Set where<br>
> HRefl : HId M M<br>
><br>
> is equivalent to<br>
><br>
> (p : Id A B) * Id{B} (coe p a) b<br>
><br>
> See<br>
> <a href="https://github.com/dlicata335/hott-agda/blob/master/misc/Heterogeneous.agda" rel="noreferrer" target="_blank">https://github.com/dlicata335/<wbr>hott-agda/blob/master/misc/<wbr>Heterogeneous.agda</a><br>
> for the main idea (I didn’t wrap with Sigma types).<br>
><br>
> Note that Id (coe p a) b is equivalent to the inductive family path-over type<br>
> PathOver (\X -> X) p a b, but I wanted to keep the file as small as possible.<br>
><br>
> I didn’t include it in the file, but we know that that Sigma-type is equivalent to Id{(A : Set) * A} (A,a) (B,a),<br>
> which is the construction Conor uses in his thesis Section 5.1.5 (<a href="http://strictlypositive.org/thesis.pdf" rel="noreferrer" target="_blank">http://strictlypositive.org/<wbr>thesis.pdf</a>)<br>
> to show that you can get heterogeneous equality from homogeneous equality with K.<br>
><br>
><br>
> Regarding UIP, it’s also constructed in Conor’s thesis, Sec 5. It’s described in the context of<br>
> equality of telescopes, but here’s the special case of telescopes of length 1, inspired by that:<br>
><br>
> Suppose you have heterogeneous equality with, as an elimination rule,<br>
> J for homogeneous instances of heterogeneous equality (i.e. J for HId {A} a {A} a’).<br>
> (Note that Agda —without-K helpfully prevents you from proving this, or else we’d be in trouble!)<br>
><br>
> From this, you get that such a homogeneous heterogeneous equality implies homogeneous equality<br>
> (without the coercion by an existentially quantified type equality), and<br>
> this will be an equivalence because both types have the same intro and elim (refl and J).<br>
> Moving along this equivalence, it suffices to prove UIP for homogeneous instances<br>
> of heterogeneous equality. This follows from<br>
><br>
> UIP1' : {A : Set} {x : A} {y : A} (p : HId {A} x {A} y) → HId {HId x x} HRefl {HId x y} p<br>
><br>
> which you can prove because using heterogeneous equality in the result gets around<br>
> the usual type checking failure that stops you from proving UIP. Then the y=x case is a<br>
> homogeneous instance of heterogeneous equality, so it can be converted to a homogeneous equality.<br>
><br>
> -Dan<br>
><br>
> > On Oct 28, 2016, at 2:36 PM, Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>> wrote:<br>
> ><br>
> ><br>
> ><br>
> > On 28/10/16 15:59, Dan Licata wrote:<br>
> >>> The idea is very similar to using heterogeneous equality, as you will<br>
> >>> see.<br>
> >><br>
> >> More precisely, I think that heterogeneous equality (a:A) == (b:B) is equivalent to either<br>
> >> (writing PathOver F p a b for your a ≡[ p ] b to make the type family explicit,<br>
> >> and writing == for the homogeneous identity type)<br>
> >><br>
> >> (p : A == B) -> PathOver (\X -> X) p a b<br>
> >><br>
> >> or<br>
> >><br>
> >> (p : A == B) * PathOver (\X -> X) p a b<br>
> >><br>
> >> depending on what the rules for the (a:A) == (b:B) type are<br>
> >> (there was a thread a few years ago about whether this should imply A==B or require A==B, but I can’t find it right now).<br>
> ><br>
> > I'd also like to understand this, and also the claim that the elimination principle for heterogeneous equality implies K.<br>
> ><br>
> > Martin<br>
> ><br>
><br>
> ______________________________<wbr>_________________<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" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
><br>
><br>
<br>
</div></div></blockquote></div><br></div>