diff --git a/HomeworkEight.idr b/HomeworkEight.idr
new file mode 100644
index 0000000..5867eba
--- /dev/null
+++ b/HomeworkEight.idr
@@ -0,0 +1,34 @@
+module HomeworkEight
+%default total
+%access public export
+
+data Exp = Var String | Abs String Exp | App Exp Exp
+
+data Occur : List String -> Exp -> Type where
+  OVar : Occur [s] (Var s)
+  OAbs : Occur xs e -> Occur xs (Abs s e)
+  OApp : Occur xs e1 -> Occur ys e2 -> Occur (xs ++ ys) (App e1 e2)
+
+occ1 : Occur ["x"] (Var "x")
+occ1 = OVar
+
+occ2 : Occur ["x"] (Abs "y" (Var "x"))
+occ2 = OAbs OVar
+
+occ3 : Occur ["x","x"] (App (Var "x") (Var "x"))
+occ3 = OApp OVar OVar
+
+occ4 : Occur ["x","x"] (Abs "x" (App (Var "x") (Var "x")))
+occ4 = OAbs occ3
+
+--
+-- -----------------
+--    [x] @ x
+--
+--      xs @ e
+-- -----------------
+--    xs @ \x . e
+--
+--  xs @ e1  ys @ e2  zs = xs ++ ys
+--  -------------------------------
+--          zs @ e1 e2
diff --git a/HomeworkFive.idr b/HomeworkFive.idr
new file mode 100644
index 0000000..6a6db21
--- /dev/null
+++ b/HomeworkFive.idr
@@ -0,0 +1,55 @@
+module HomeworkFive
+import HomeworkFour
+%default total
+
+zeroEven : even Z = True
+zeroEven = Refl
+
+twoEven : even (S (S Z)) = True
+twoEven = Refl
+
+threeOdd : even (S (S (S Z))) = False
+threeOdd = Refl
+
+fourEven : even (S (S (S (S Z)))) = True
+fourEven = Refl
+
+xor : Bool -> Bool -> Bool
+xor True p = not p
+xor False p = p
+
+xorNot : b1 = b2 -> xor (not b1) b2 = True
+xorNot {b1=True} Refl = Refl
+xorNot {b1=False} Refl = Refl
+
+xorEq : xor (not b1) b2 = b1 == b2
+xorEq {b1=True} {b2=True} = Refl
+xorEq {b1=True} {b2=False} = Refl
+xorEq {b1=False} {b2=True} = Refl
+xorEq {b1=False} {b2=False} = Refl
+
+plusE : even n = bn -> even m = bm -> even (n+m) = (xor (not bn) bm)
+plusE {n=Z} Refl p = p
+plusE {n=S Z} Refl p = evenFlip p
+plusE {n=S (S m)} p1 p2 = plusE {n=m} p1 p2
+
+plusEE : even n = True -> even m = True -> even (n+m) = True
+plusEE = plusE
+
+plusOE : even n = False -> even m = True  -> even (n+m) = False
+plusOE = plusE
+
+plusEO : even n = True  -> even m = False -> even (n+m) = False
+plusEO = plusE
+
+plusOO : even n = False -> even m = False -> even (n+m) = True
+plusOO = plusE
+
+plusEvenOdd : even n = even m -> even (n+m) = True
+plusEvenOdd p = replace (xorNot (sym p)) $ plusE p (sym p)
+
+plusEvenOdd' : even n = x -> even m = y -> even (n+m) = x==y
+plusEvenOdd' p1 p2 = replace xorEq (plusE p1 p2)
+
+plusEvenOdd'' : even n = x -> even m = y -> x = y -> even (n+m) = True
+plusEvenOdd'' Refl Refl eq = plusEvenOdd eq
diff --git a/HomeworkFour.idr b/HomeworkFour.idr
new file mode 100644
index 0000000..976d0b8
--- /dev/null
+++ b/HomeworkFour.idr
@@ -0,0 +1,39 @@
+module HomeworkFour
+%default total
+%access public export
+
+even : Nat -> Bool
+even Z = True
+even (S Z) = False
+even (S (S n)) = even n
+
+evenSuc : even n = True -> even (S n) = False
+evenSuc {n=Z} Refl = Refl
+evenSuc {n=S Z} Refl impossible
+evenSuc {n=S (S m)} p = evenSuc {n=m} p
+
+oddSuc : even n = False -> even (S n) = True
+oddSuc {n=Z} Refl impossible
+oddSuc {n=S Z} Refl = Refl
+oddSuc {n=S (S m)} p = oddSuc {n=m} p
+
+evenFlip : even n = b -> even (S n) = not b
+evenFlip {n=Z} Refl = Refl
+evenFlip {n=S Z} Refl = Refl
+evenFlip {n=S (S m)} p = evenFlip {n=m} p
+
+evenFlip' : even n = b -> even (S n) = not b
+evenFlip' {b=True} p = evenSuc p
+evenFlip' {b=False} p = oddSuc p
+
+evenSucSuc : even n = True -> even (S (S n)) = True
+evenSucSuc p = p
+
+oddSucSuc : even n = False -> even (S (S n)) = False
+oddSucSuc p = p
+
+evenStay : even n = b -> even (S (S n)) = b
+evenStay p = p
+
+evenStayEq : even n = even (S (S n))
+evenStayEq = Refl
diff --git a/HomeworkNine.idr b/HomeworkNine.idr
new file mode 100644
index 0000000..fd30422
--- /dev/null
+++ b/HomeworkNine.idr
@@ -0,0 +1,23 @@
+module HomeworkNine
+import HomeworkEight
+%default total
+
+remove : Eq a => a -> List a -> List a
+remove x = filter (/=x)
+
+data FV : List String -> Exp -> Type where
+  FVar : FV [s] (Var s)
+  FAbs : FV xs e -> FV (remove s xs) (Abs s e)
+  FApp : FV xs e1 -> FV ys e2 -> FV (xs ++ ys) (App e1 e2)
+
+fv1 : FV ["x"] (Var "x")
+fv1 = FVar
+
+fv2 : FV ["x"] (Abs "y" (Var "x"))
+fv2 = FAbs FVar
+
+fv3 : FV ["x","x"] (App (Var "x") (Var "x"))
+fv3 = FApp FVar FVar
+
+fv4 : FV [] (Abs "x" (App (Var "x") (Var "x")))
+fv4 = FAbs fv3
diff --git a/HomeworkSeven.idr b/HomeworkSeven.idr
new file mode 100644
index 0000000..de8d511
--- /dev/null
+++ b/HomeworkSeven.idr
@@ -0,0 +1,25 @@
+module HomeworkSeven
+%default total
+
+data Tree = Node String Tree Tree | Leaf
+
+data Height : Tree -> Nat -> Type where
+  HLeaf : Height Leaf 1
+  HNode : Height t1 n1 -> Height t2 n2 -> Height (Node s t1 t2) (S (max n1 n2))
+
+e1 : Height (Node "a" Leaf Leaf) 2
+e1 = HNode HLeaf HLeaf
+
+e2 : Height (Node "b" Leaf (Node "a" Leaf Leaf)) 3
+e2 = HNode HLeaf e1
+
+e3 : Height (Node "c" (Node "b" Leaf (Node "a" Leaf Leaf)) Leaf) 4
+e3 = HNode e2 HLeaf
+
+--
+-- -------------
+--   Leaf ^ 1
+--
+-- t1 ^ n1  t2 ^ n2  n = 1 + max(n1,n2)
+-- ------------------------------------
+--         Tree s t1 t2 ^ n
diff --git a/HomeworkSix.idr b/HomeworkSix.idr
new file mode 100644
index 0000000..2efc9c2
--- /dev/null
+++ b/HomeworkSix.idr
@@ -0,0 +1,20 @@
+module HomeworkSix
+%default total
+
+data Term = Tru | Fls | Not Term | Cond Term Term Term 
+
+data OT : Term -> Type where
+  OptNotNot : OT (Not (Not t))
+  OptNot : OT t -> OT (Not t)
+  OptCond1 : OT t1 -> OT (Cond t1 t2 t3)
+  OptCond2 : OT t2 -> OT (Cond t1 t2 t3)
+  OptCond3 : OT t3 -> OT (Cond t1 t2 t3)
+
+p1 : OT (Cond (Not Tru) (Not (Not Tru)) Fls)
+p1 = OptCond2 OptNotNot
+
+p2 : OT (Not (Not (Not Fls)))
+p2 = OptNotNot
+
+p3 : OT (Not (Cond (Not Tru) (Not (Not Tru)) Fls))
+p3 = OptNot p1