<div dir="ltr">Hi,<div><br></div><div>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:</div><div><br></div><div><div>data AndEquals : (A : Set) (B : Set) (a : A) (b : B) → Set where</div><div> and-refl : {A : Set} {B : Set} {a : A} {b : B} (fst : A ≡ B) (snd : a ≡ b) → AndEquals A B a b</div></div><div><br></div><div>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".</div><div><br></div><div>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.</div><div><br></div><div>Is the above definition substantially different than heterogeneous equality?</div><div><br></div><div>Does anyone have advice for how it could be made to type-check?</div><div><br></div><div>Best,</div><div>Owen</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, Oct 28, 2016 at 10:23 PM, 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,<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>
<span class="HOEnZb"><font color="#888888"><br>
-Dan<br>
</font></span><div class="HOEnZb"><div class="h5"><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>
</div></div></blockquote></div><br></div>