-- Simply-typed lambda definability and normalization by evaluation
-- formalized in Agda
--
-- Author: Andreas Abel, May/June 2018

module Everything where

-- 0. Standard library imports and auxiliary definitions

import Library

-- 1. A universe of simple types; contexts and order-preserving embeddings

import SimpleTypes

-- 2. Simply-typed lambda calculus (STLC) definability:
-- 2a. STLC-definability via Kripke predicates for STLC with constants
-- 2b. Intrinsically typed variables and terms and their interpretation
-- 2c. Reflect/reify: a term model proving that soundness of definability
-- 2d. Fundamental theorem of logical relations proving completeness

import STLCDefinable

-- 3. Adapting reflection/reification to obtain normalization

import NBE

-- 4. Using Kripke predicates to refute STLC-definability...
-- 4a. ... of boolean negation

import NotNotDefinable

-- 4b. ... of an inhabitant of Peirce's formula

import PeirceNotDefinable