Universes.agda

module Introduction.Universes where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

postulate IsEven : Nat -> Prop

data Even : Set where
  even : (n : Nat) -> IsEven n -> Even