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>