Ok, thanks!<br><br><div class="gmail_quote">2013/1/23 Dan Rosén <span dir="ltr">&lt;<a href="mailto:danr@student.chalmers.se" target="_blank">danr@student.chalmers.se</a>&gt;</span><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
A remark, if you want to have something like decidable equality on<br>
types, you could encode a universe. There is much literature about<br>
this, one good starting point could be Stevan Andjelkovic&#39;s Master&#39;s<br>
Thesis: <a href="http://publications.lib.chalmers.se/records/fulltext/146810.pdf" target="_blank">http://publications.lib.chalmers.se/records/fulltext/146810.pdf</a>,<br>
see chapter 3 and onwards.<br>
<br>
Best,<br>
Dan<br>
<div class="im HOEnZb"><br>
On Mon, Jan 21, 2013 at 8:01 PM, Daniel Peebles &lt;<a href="mailto:pumpkingod@gmail.com">pumpkingod@gmail.com</a>&gt; wrote:<br>
&gt; I&#39;m pretty sure it shouldn&#39;t be possible to do that in Idris (if it is, it&#39;s<br>
&gt; probably a bug), and I don&#39;t think most people want it in Agda either. The<br>
&gt; main reason it&#39;s undesriable is that it violates parametricity, which is a<br>
&gt; property most FP people really want.<br>
&gt;<br>
&gt;<br>
&gt; On Mon, Jan 21, 2013 at 12:58 PM, Dmytro Starosud &lt;<a href="mailto:d.starosud@gmail.com">d.starosud@gmail.com</a>&gt;<br>
&gt; wrote:<br>
&gt;&gt;<br>
</div><div class="HOEnZb"><div class="h5">&gt;&gt; Hello guys,<br>
&gt;&gt;<br>
&gt;&gt; In Idris one can write:<br>
&gt;&gt;<br>
&gt;&gt; g : Type -&gt; Bool<br>
&gt;&gt; g Int = True<br>
&gt;&gt; g _ = False<br>
&gt;&gt;<br>
&gt;&gt; Is it possible to do the same in Agda, in particular:<br>
&gt;&gt;<br>
&gt;&gt; type-dec : (A B : Set) -&gt; Dec (A \equiv B)<br>
&gt;&gt; type-dec = ?<br>
&gt;&gt;<br>
&gt;&gt; Thanks in advance!<br>
&gt;&gt;<br>
</div></div><div class="HOEnZb"><div class="h5">&gt;&gt; _______________________________________________<br>
&gt;&gt; Agda mailing list<br>
&gt;&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt;&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;&gt;<br>
&gt;<br>
</div></div></blockquote></div><br>