diff --git a/chapter4/Types.idr b/chapter4/Types.idr
index c8ace65..78c7336 100644
--- a/chapter4/Types.idr
+++ b/chapter4/Types.idr
@@ -114,3 +114,27 @@ maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
 maxMaybe Nothing y = y
 maxMaybe x Nothing = x
 maxMaybe a@(Just x) b@(Just y) = if x > y then a else b
+
+
+data PowerSource = Petrol | Pedal
+data Vehicle : PowerSource -> Type where
+  Bicycle : Vehicle Pedal
+  Car : (fuel : Nat) -> Vehicle Petrol
+  Bus : (fuel : Nat) -> Vehicle Petrol
+  -- exercise
+  Unicycle : Vehicle Pedal
+  Motorcycle : (fuel : Nat) -> Vehicle Petrol
+
+wheels : Vehicle power -> Nat
+wheels Bicycle = 2
+wheels (Car fuel) = 4
+wheels (Bus fuel) = 4
+wheels Unicycle = 1
+wheels (Motorcycle fuel) = 2
+
+refuel : Vehicle Petrol -> Vehicle Petrol
+refuel (Car fuel) = Car 100
+refuel (Bus fuel) = Bus 200
+refuel (Motorcycle fuel) = Motorcycle 100
+refuel Bicycle impossible
+refuel Unicycle impossible
diff --git a/chapter4/Vect.idr b/chapter4/Vect.idr
new file mode 100644
index 0000000..e0aa19c
--- /dev/null
+++ b/chapter4/Vect.idr
@@ -0,0 +1,40 @@
+module Vector
+
+import Data.Fin
+
+data Vect : Nat -> Type -> Type where
+  Nil : Vect Z a
+  (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a
+
+%name Vect xs, ys, zs
+
+append : Vect n elem -> Vect m elem -> Vect (n + m) elem
+append [] ys = ys
+append (x :: xs) ys = x :: append xs ys
+
+
+length : Vect n elem -> Nat
+length {n} xs = n
+
+zip : Vect n a -> Vect n b -> Vect n (a, b)
+zip [] [] = []
+zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys
+
+index : Fin n -> Vect n elem -> elem
+index FZ (x :: xs) = x
+index (FS k) (x :: xs) = index k xs
+
+tryIndex : Integer -> Vect n a -> Maybe a
+tryIndex {n} i xs = case integerToFin i n of
+                     Nothing => Nothing
+                     (Just idx) => Just (index idx xs)
+
+
+vectTake : (m : Fin n) -> Vect n elem -> Vect (finToNat m) elem
+vectTake FZ xs = []
+vectTake (FS k) (x :: xs) = x :: vectTake k xs
+
+sumEntries : Num a => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
+sumEntries {n} pos xs ys = case integerToFin pos n of
+                                Nothing => Nothing
+                                (Just idx) => Just ((index idx xs) + (index idx ys))