diff --git a/tutorial/02.1-Relevance.ua b/tutorial/02.1-Relevance.ua
new file mode 100644
--- /dev/null
+++ b/tutorial/02.1-Relevance.ua
@@ -0,0 +1,61 @@
+-- Relevance levels and erasure
+---------------------------------
+
+-- In uAgda, each term can exist at a specific relevance. 
+-- 
+-- For example * is the most relevant level, *< is less relevant, etc.
+-- 
+-- The idea is that a term less relevant worlds can be erased, and the
+-- terms remains meaningful.
+
+
+-- For example, we can use a more precise type of the Leibniz equality
+-- that says that the actual type used is irrelevant for the predicate:
+
+Eq = \ A a b -> (P : A -> *) -> P a -> P b
+     : (A : *<) -> (a b : A) -> *1,
+
+-- Another example is the following: the inductive principle for
+-- natural numbers is independent on the actual representation of the
+-- naturals, so they are irrelevant.  This can be expressed as
+-- follows:
+
+-- We assume an (abstract) representation N of naturals, in a less
+-- relevant world, as well as constructors for successor and zero.
+
+Nat = \(N : *<) (s : N -> N) (z : N) ->
+
+-- Then define the induction principle as normal (the predicate is in *)
+\(n : N) -> (P : N -> *) -> P z -> ((m : N) -> P m -> P (s m)) -> P n,
+
+
+-- We know that all the programs we have written using naturals
+-- satisfying the above induction principle can be represented by
+-- Naturals where the irrelevant parts are erased. We can access this
+-- erasure within uAgda by using the % operator. The second argument
+-- is the first world of relevance to erase (all less relevant worlds
+-- will be erased as well).
+
+Nat-representation = Nat % 1,
+
+-- The normal form of the above term reveals that the result is the
+-- usual Church encoding for naturals.
+
+
+-- Each term can be copied to a less relevant world:
+
+shiftType = \A -> A<
+          : * -> *<,
+
+shiftValue 
+  = \ A a -> a<
+  : (A : *) -> (a : A) -> A<,
+
+
+-- In summary, occurences of the < operator can be understood as
+-- relevance annotations. They can be used mark types, terms and their
+-- usage as irrelevant. They are useful for erasure, but may be safely
+-- ignored otherwise.
+
+
+*
diff --git a/tutorial/03-Parametricity.ua b/tutorial/03-Parametricity.ua
--- a/tutorial/03-Parametricity.ua
+++ b/tutorial/03-Parametricity.ua
@@ -33,9 +33,11 @@
 -- parametricity and erasure. See the following reference for
 -- the explanation:
 
--- https://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=127466
+-- http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=127466
 
 fparam2 = f!!%2 : (x y : A<) -> A!!%2 x y -> B!!%2 (f< x) (f< y),
+
+
 
 
 *)
diff --git a/tutorial/03.1-Parametricity-Use.ua b/tutorial/03.1-Parametricity-Use.ua
new file mode 100644
--- /dev/null
+++ b/tutorial/03.1-Parametricity-Use.ua
@@ -0,0 +1,26 @@
+-- let's use parametricity in a useful way: prove that any
+-- function of type (X : *) -> X -> X is the identity.
+
+-- To simplify the example we use impredicativity here, use
+-- the -I flag to enable it.
+
+Eq = \A a b -> (P : A -> *) -> P a -> P b
+   : (A : *<) -> A -> A -> *
+   ,
+
+Theorem = 
+  (f : (A : *) -> A -> A) ->
+  (A : *) ->
+  (x : A) ->
+  Eq A< x< (f A x)<,
+
+
+proof = \(f : (A : *) -> (a : A) -> A) ->
+        \(A : *) ->
+        \(x : A) -> f! A< (Eq A< x<) x< (\_ p -> p)
+      : Theorem
+
+
+,
+* 
+
diff --git a/uAgda.cabal b/uAgda.cabal
--- a/uAgda.cabal
+++ b/uAgda.cabal
@@ -1,5 +1,5 @@
 name:           uAgda
-version:        1.0.0.1
+version:        1.0.0.2
 category:       Dependent Types
 synopsis:       A simplistic dependently-typed language with parametricity.
 description:
@@ -28,7 +28,9 @@
      tutorial/00-Start-Here.ua
      tutorial/01-Module.ua
      tutorial/02-Holes.ua
+     tutorial/02.1-Relevance.ua
      tutorial/03-Parametricity.ua
+     tutorial/03.1-Parametricity-Use.ua
      tutorial/04-Data.ua