diff --git a/ZeroToLean/TheoremProvingInLean4/Chapter01_Introduction/intro.lean b/ZeroToLean/TheoremProvingInLean4/Chapter01_Introduction/intro.lean
new file mode 100644
index 0000000..ae7dbbf
--- /dev/null
+++ b/ZeroToLean/TheoremProvingInLean4/Chapter01_Introduction/intro.lean
@@ -0,0 +1,7 @@
+namespace Introduction
+  theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p :=
+   fun hpq : p ∧ q =>
+     have hp : p := And.left hpq
+     have hq : q := And.right hpq
+     show q ∧ p from And.intro hq hp
+end Introduction
diff --git a/ZeroToLean/TheoremProvingInLean4/Chapter02_DependentTypeTheory/simplyTypeTheory.lean b/ZeroToLean/TheoremProvingInLean4/Chapter02_DependentTypeTheory/simplyTypeTheory.lean
new file mode 100644
index 0000000..d80e354
--- /dev/null
+++ b/ZeroToLean/TheoremProvingInLean4/Chapter02_DependentTypeTheory/simplyTypeTheory.lean
@@ -0,0 +1,152 @@
+namespace simpleTypeTheory
+
+-- some are pasted from the book and some are just me testing stuff
+
+/- Define some constants. -/ 
+def m : Nat := 1 -- m is a natural number 
+def n : Nat := 0
+def b1 : Bool := true -- b1 is a Boolean 
+def b2 : Bool := false
+/- Check their types. -/ 
+#check m -- output: Nat 
+#check n 
+#check n + 0 -- Nat 
+#check m * (n + 0) -- Nat 
+#check b1 -- Bool 
+#check b1 && b2 -- "&&" is the Boolean and 
+#check b1 || b2 -- Boolean or 
+#check true -- Boolean "true" 
+/- Evaluate -/ 
+#eval 5 * 4 
+#eval m + 2 
+#eval b1 && b2 ------20 3 false
+
+
+def t : Bool := true
+def f : Bool := false
+
+#eval t ∧ f ∨ (t ∨ f)
+
+
+#check Nat → Nat
+#check Nat -> Nat
+-- type the arrow as "\to" or "\r"
+-- alternative ASCII notation
+#check Nat × Nat
+#check Prod Nat Nat
+-- type the product as "\times"
+-- alternative notation
+#check Nat → Nat → Nat
+
+#check Nat → (Nat → Nat)
+ -- same type as above
+#check Nat × Nat → Nat
+#check (Nat → Nat) → Nat -- a "functional"
+#check Nat.succ
+#check (0, 1)
+#check Nat.add
+-- Nat → Nat
+-- Nat × Nat
+-- Nat → Nat → Nat
+#check Nat.succ 2
+ -- Nat
+#check Nat.add 3
+ -- Nat → Nat
+#check Nat.add 5 2
+ -- Nat
+#check (5, 9).1
+ -- Nat
+#check (5, 9).2
+ -- Nat
+#eval Nat.succ 2
+ -- 3
+#eval Nat.add 5 2
+ -- 7
+#eval (5, 9).1
+ -- 5
+#eval (5, 9).2
+ -- 9
+
+#check Nat
+ -- Type
+#check Bool
+ -- Type
+#check Nat → Bool
+ -- Type
+#check Nat × Bool
+ -- Type
+#check Nat → Nat
+ -- ...
+#check Nat × Nat → Nat
+#check Nat → Nat → Nat
+#check Nat → (Nat → Nat)
+#check Nat → Nat → Bool
+#check (Nat → Nat) → Nat
+
+
+def α : Type := Nat
+def β : Type := Bool
+def F : Type → Type := List
+def G : Type → Type → Type := Prod
+#check α
+ -- Type
+#check F α
+ -- Type
+#check F Nat
+ -- Type
+#check G α
+ -- Type → Type
+#check G α β
+ -- Type
+#check G α Nat
+ -- Type
+
+
+def α : Type := Nat 
+#check List α -- Type 
+#check List Nat -- Type
+
+#check List
+
+end simpleTypeTheory
+
+namespace FunctionAbstractionAndEvaluation
+#check fun (x : Nat) => x + 5 -- Nat → Nat #check λ (x : Nat) => x + 5 -- λ and fun mean the same thing #check fun x => x + 5 -- Nat inferred #check λ x => x + 5 -- Nat inferred
+
+#eval (λ x : Nat => x + 5) 10 -- 15
+
+#check fun (x : Nat) => x + 5
+ -- Nat → Nat
+#check λ (x : Nat) => x + 5
+ -- λ and fun mean the same thing
+#check fun x => x + 5
+ -- Nat inferred
+#check λ x => x + 5
+ -- Nat inferred
+
+def f (n : Nat) : String := toString n
+def g (s : String) : Bool := s.length > 0
+#check fun x : Nat => x
+ -- Nat → Nat
+#check fun x : Nat => true
+ -- Nat → Bool
+#check fun x : Nat => g (f x)
+ -- Nat → Bool
+#check fun x => g (f x)
+ -- Nat → Bool
+
+ #check fun (g : String → Bool) (f : Nat → String) (x : Nat) => g (f x)
+-- (String → Bool) → (Nat → String) → Nat → Bool
+
+#check fun (α β γ : Type) (g : β → γ) (f : α → β) (x : α) => g (f x)
+
+#check (fun x : Nat => x) 1
+ -- Nat
+#check (fun x : Nat => true) 1
+ -- Bool
+#check (fun (α β γ : Type) (u : β → γ) (v : α → β) (x : α) => u (v x)) Nat String Bool g f 0
+-- Bool
+
+ -- gonna try 10p / day. stopped at 11 Definitions.
+
+end FunctionAbstractionAndEvaluation