Think of this like quoting and eval in Lisp. The type "expression of type U" might work with operations like eval: "expression of type U" -> U quote: U

Think of this like quoting and eval in Lisp. The type "expression of type U" might work with operations like eval: "expression of type U" -> U quote: U -> "expression of type U" chriswarbo's reply higher up should be taken to supersede my reply -- he's obviously more current on this stuff.