[Agda] Type decidability

[Dan Rosén]

A remark, if you want to have something like decidable equality on
types, you could encode a universe. There is much literature about
this, one good starting point could be Stevan Andjelkovic's Master's
Thesis: http://publications.lib.chalmers.se/records/fulltext/146810.pdf,
see chapter 3 and onwards.

Best,
Dan

On Mon, Jan 21, 2013 at 8:01 PM, Daniel Peebles <pumpkingod at gmail.com> wrote:
> I'm pretty sure it shouldn't be possible to do that in Idris (if it is, it's
> probably a bug), and I don't think most people want it in Agda either. The
> main reason it's undesriable is that it violates parametricity, which is a
> property most FP people really want.
>
>
> On Mon, Jan 21, 2013 at 12:58 PM, Dmytro Starosud <d.starosud at gmail.com>
> wrote:
>>
>> Hello guys,
>>
>> In Idris one can write:
>>
>> g : Type -> Bool
>> g Int = True
>> g _ = False
>>
>> Is it possible to do the same in Agda, in particular:
>>
>> type-dec : (A B : Set) -> Dec (A \equiv B)
>> type-dec = ?
>>
>> Thanks in advance!
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>