{-# OPTIONS --experimental-irrelevance #-}

-- {-# OPTIONS -v tc.univ:100 -v tc.meta:100 #-}
-- {-# OPTIONS -v tc.rec:100 #-}

-- Andreas, 2011-04-27 universe levels can be made irrelevant
-- Ulf 2011-10-03. No they can't. How is that even consistent?
-- Andreas, 2011-10-03. Yes, they can!
--   .(i : Level)(A : Set i)   does not mean that Set i = Set j for all i,j
-- but nl i A = nl j A  for all i,j.

module IrrelevantLevel where

open import Common.Level

postulate
  Lst : .(i : Level)(A : Set i) → Set i
  nl  : .(i : Level)(A : Set i) → Lst i A
  cns : .(i : Level)(A : Set i) → A → Lst i A → Lst i A


data List .(i : Level)(A : Set i) : Set i where
  nil  : List i A
  cons : A → List i A → List i A

singleton : .{i : Level}{A : Set i}(a : A) → List i A
singleton a = cons a nil

record Wrap .(i : Level)(A : Set i) : Set i where
  field
    wrap : A

module M .(i : Level)(A : Set i) where

  data Li : Set i where
    ni : Li
    co : A → Li → Li
