diff --git a/src/LambdaPi.agda b/src/LambdaPi.agda
index c372c01b..e959807a 100644
--- a/src/LambdaPi.agda
+++ b/src/LambdaPi.agda
@@ -78,4 +78,4 @@ progress : ∀ {M A} → ∅ ⊢ M ⦂ A → Progress M
 ----------------------------------------------------
 -- preservation
 ----------------------------------------------------
-preserve : ∀ {M N A} → ∅ ⊢ M ⦂ A → M —→ N → ∅ ⊢ N ⦂ A
\ No newline at end of file
+preserve : ∀ {M N A} → ∅ ⊢ M ⦂ A → M —→ N → ∅ ⊢ N ⦂ A
diff --git a/src/Project/Lambda1.agda b/src/Project/Lambda1.agda
new file mode 100644
index 00000000..f3fb6396
--- /dev/null
+++ b/src/Project/Lambda1.agda
@@ -0,0 +1,19 @@
+module Project.Lambda1 where
+
+open import Data.Nat using (ℕ; suc; _≟_)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Nullary using (yes; no; ¬_)
+
+data Term : Set where
+  `_ : ℕ →  Term
+  ƛ_ : Term →  Term
+  _·_ : Term →  Term →  Term
+
+  `suc _ : Term →  Term
+  `zero : Term
+
+data Value : Term →  Set where
+  V-ƛ : ∀ {N} →  Value (ƛ N)
+
+data Context : Set where
+  ⊙ : Context