module Sort (A : Set) (_<_ : A @$\rightarrow$@ A @$\rightarrow$@ Bool) where
sort : List A @$\rightarrow$@ List A
sort = -- 実装は省略 ...

-- Parameterized Module により N.sort や B.sort が可能
open import Sort Nat  Nat._<_  as N
open import Sort Bool Bool._<_ as B