[Agda] Re: Builtins

[Kirill Elagin]

On Sat, Apr 25, 2015 at 9:32 PM N. Raghavendra <raghu at hri.res.in> wrote:

> Many thanks for the clear explanation.  I have one more question about
> judgemental equality.  Namely, suppose I have two terms a and b of the
> same type A, and suppose that the following thing type-checks:
>
> theorem : a ≡ b
> theorem = refl
>
> where ≡ are as in Relation.Binary.Core.  Does it mean then that a is
> judgementally equal to b?
>

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`).

`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).

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).
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150425/897429e1/attachment-0001.html