Идрис - определить интерфейс динамически

Question

Есть ли способ построить реализацию интерфейса "динамически"? У меня есть код, который выглядит как

record MySemigroup where
  constructor MkMySemigroup
  set : Type
  op  : set -> set -> set

mySemigroupIsSemigroup : (s : MySemigroup) -> Semigroup (set s)
mySemigroupIsSemigroup s = ?hole

и я хотел бы определить экземпляр Semigroup на set s, используя op s.