Quotation.

Take a Value back to Term.

Or more precisely

• ValueIntro to TermChk
• ValueElim to TermInf

Unlike LambdaPi, our Value has Eq instance. Therefore we don't need quotation for type-checker. It's sometimes useful anyway.

>>> t <- type_ emptyCtx systemfIdentity >>= errorlessValueIntro' . snd
>>> prettyPut t
∀ a → a → a

>>> :t t
t :: ValueIntro Void SystemF Sym

>>> prettyPut (quote_ t)
∀ a → a → a

>>> :t quote_ t
quote_ t :: TermChk SystemF Sym

>>> t' <- check_ emptyCtx (quote_ t) (sort_ SysFStar) >>= errorlessValueIntro'
>>> prettyPut t'
∀ a → a → a