Hello guys,<br><br>In Idris one can write:<br><pre>g : Type -&gt; Bool
g Int = True
g _ = False</pre>Is it possible to do the same in Agda, in particular:<br><pre>type-dec : (A B : Set) -&gt; Dec (A \equiv B)<br>type-dec = ?<br></pre>Thanks in advance!<br>