title: Idris - define interface dynamically
body: <p>Is there a way to build the implementation of an interface &quot;dynamically&quot;?
  I have some code which looks like</p>
  <pre><code>record MySemigroup where
    constructor MkMySemigroup
    set : Type
    op  : set -&gt; set -&gt; set
    
  mySemigroupIsSemigroup : (s : MySemigroup) -&gt; Semigroup (set s)
  mySemigroupIsSemigroup s = ?hole
  </code></pre>
  <p>and I would like to define the instance of <code>Semigroup</code> on <code>set s</code> using <code>op s</code>.</p>