{-# 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