A parser, type checker and evaluator for a type theory with universe polymorphism