(* Note: sort evaluation *)
   sv: nat → dd;

(* Note: interpretation: sort *)
   ms: ∀gv,lv,s. ⟦⋆s⟧{M}[gv, lv] ≗ sv M s;