{-# OPTIONS --without-K #-}

module README where

-- NbE for Martin-Löf type theory with a cumulative universe hierarchy using an untyped domain model
--   with a completeness and a soundness theorems
import Cumulative.README

-- NbE for Martin-Löf type theory with a non-cumulative universe using an untyped domain model
--   with a completeness and a soundness theorems
import NonCumulative.README