{-# OPTIONS --without-K #-} module Unbox.README where open import Level using (0ℓ) open import Axiom.Extensionality.Propositional -- we have to postulate functional extensionality to prove properties about evaluation environments. postulate fext : Extensionality 0ℓ 0ℓ -- static semantics open import Unbox.Statics -- nbe based on a presheaf model open import Unbox.Presheaf -- nbe based on an untyped domain open import Unbox.Semantics -- completeness for nbe open import Unbox.PER fext -- soundness for nbe open import Unbox.Soundness fext