-- 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.


*