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 "f refl", because A and B is known at compile time and if "op A ≡ op B" is inhabited then "refl" is enough, I mean I don't need to write complex proof.<br>
But "op B : Set" is undecidable, so I cannot make that proof implicit, and also I cannot make it inferable (Agda not always wants to infer "refl" even if "op A" is exactly the same as "op B").<br>
<br>Is there any way to substitute "f refl" with some "g"? I mean something like C-style macros:<br>#define g (f refl)<br><br>Thanks in advance,<br>Dmytro <br>