I might be not clear enough.<br>Could you please refer to this (<a href="https://github.com/dima-starosud/Uniqueness-typing-in-Agda/blob/master/HandleAPITest.agda" target="_blank">https://github.com/dima-starosud/Uniqueness-typing-in-Agda/blob/master/HandleAPITest.agda</a>).<br>

I want to get rid of:<br><pre>⇒⟦ refl ⟧⇒</pre>e.g. replace it with &quot;then&quot;, which would mean semicolon just like in imperative program<br><br>Best regards,<br>Dmytro <br><br><div class="gmail_quote">2013/2/1 Dmytro Starosud <span dir="ltr">&lt;<a href="mailto:d.starosud@gmail.com" target="_blank">d.starosud@gmail.com</a>&gt;</span><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello list,<br><br>I have the following code (simplified).<br><br>A B : Set<br><br>Ty : Set → Set → Set<br>op : Set → Set<br>
<br>f : ∀ {A B} → op A ≡ op B → Ty A B → Ty B A<br>x : Ty A B<br><br>y = f refl x<br><br>I should always write &quot;f refl&quot;, because A and B is known at compile time and if &quot;op A ≡ op B&quot; is inhabited then &quot;refl&quot; is enough, I mean I don&#39;t need to write complex proof.<br>

But &quot;op B : Set&quot; is undecidable, so I cannot make that proof implicit, and also I cannot make it inferable (Agda not always wants to infer &quot;refl&quot; even if &quot;op A&quot; is exactly the same as &quot;op B&quot;).<br>

<br>Is there any way to substitute &quot;f refl&quot; with some &quot;g&quot;? I mean something like C-style macros:<br>#define g (f refl)<br><br>Thanks in advance,<br>Dmytro <br>
</blockquote></div><br>