{-# OPTIONS --without-K #-} module README where -- Various normalization method for STLC import STLC.README -- NbE for System T using an untyped domain model -- with a completeness and a soundness theorems import T.README -- NbE for minimal STLC, a reduced version of the previous one -- with a completeness and a soundness theorems import Minimal.README -- NbE for λ□ using an untyped domain model and a presheaf model -- with a completeness and a soundness theorems for the untyped domain model import Unbox.README -- NbE for layered modal type theory using a presheaf model import Layered.README -- NbE for layered modal type theory using a presheaf model import CLayered.README -- NbE for Martin-Löf type theory using an untyped domain model -- with a completeness and a soundness theorems import MLTT.README -- NbE for Martin-Löf type theory with non cumulative universe using an untyped domain model -- with a completeness and a soundness theorems import NonCumulative.README -- NbE for Mint, a modal intuitionistic type theory, using an untyped domain model -- with a completeness and a soundness theorems import Mint.README