-- Normalization by Evaluation for Intuitionistic Predicate Logic (IPL) module Everything where -- Imports from the standard library and simple definitions import Library -- Types and terms of IPL import Formulas import Derivations -- Beth model import TermModel import NfModel -- A variant where Cover : PSh → PSh import NfModelCaseTree -- Presented at ITC 2018-07-19 import NfModelCaseTreeConv -- A generalization to any CoverMonad which includes the -- continuation monad used in Danvy's algorithm import NfModelMonad import Consistency -- A monadic interpreter using shift/reset and an optimization import DanvyShiftReset import DanvyShiftResetLiftable -- SET-interpretation and soundness of NbE import Interpretation import NbeModel -- A general theory of sheaves over preorders import PresheavesAndSheaves