signature UniversalType = sig type t val embed: unit -> ('a -> t) * (t -> 'a option) end
HOL 4, Kananaskis-14