module Sort (A : Set) (_<_ : A -> A -> Bool) where
  sort : List A -> List A
  sort = ...

open import Sort Nat  Nat._<_  as N
open import Sort Bool Bool._<_ as B