<div dir="ltr"><div class="gmail_quote">On Sat, Apr 25, 2015 at 9:32 PM N. Raghavendra <<a href="mailto:raghu@hri.res.in">raghu@hri.res.in</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Many thanks for the clear explanation. I have one more question about<br>
judgemental equality. Namely, suppose I have two terms a and b of the<br>
same type A, and suppose that the following thing type-checks:<br>
<br>
theorem : a ≡ b<br>
theorem = refl<br>
<br>
where ≡ are as in Relation.Binary.Core. Does it mean then that a is<br>
judgementally equal to b?<br></blockquote><div><br></div><div>Yes, this follows from the definition of `_≡_` and `refl` (I mean, this is not true in general, but true e.g. for stdlib’s definition of `_≡_` and `refl`).<br><br></div><div>`refl` has type `{x : A} -> x ≡ x`. If your theorem type-checks, and we know that `refl {x} : a ≡ b`, there is only one way how this can be true—if `x` is `a` and `x` is b, from which it follows that `a` is `b`. I used “is” here when referring to judgmental equality to stress again that in Agda everything is up to judgmental equality, and there is no way to tell apart judgmentally equal things (at least inside the theory).<br><br></div><div>Also note, that in Agda’s stdlib from `a ≡ b` it follows that `a` is `b`, as Agda knows that there is no other than `refl` way to construct a proof of `a ≡ b`. You said you are going to do HoTT, so you should be aware that this is not true in HoTT (since there are types that are not 0-types).<br></div></div></div>