diff --git a/src/core/t_printer.ml b/src/core/t_printer.ml
index 63178cc6..1b45dcfc 100644
--- a/src/core/t_printer.ml
+++ b/src/core/t_printer.ml
@@ -45,8 +45,8 @@ let expr_pp_with_ ~max_depth ~max_nodes ~hooks out (e : term) : unit =
     let hook_fired = List.exists (fun h -> h ~recurse:pp' out e) hooks in
     if not hook_fired then (
       match Term.view e with
-      | E_type 0 -> Fmt.string out "Type"
-      | E_type i -> Fmt.fprintf out "Type(%d)" i
+      | E_type lvl when Level.is_one lvl -> Fmt.string out "Type"
+      | E_type lvl -> Fmt.fprintf out "Type.{%a}" Level.pp lvl
       | E_var v -> Fmt.string out (Var.name v)
       (* | E_var v -> Fmt.fprintf out "(@[%s : %a@])" v.v_name pp v.v_ty *)
       | E_bound_var v ->
diff --git a/src/core/t_trace_reader.ml b/src/core/t_trace_reader.ml
index e2f8ceac..4156e1e0 100644
--- a/src/core/t_trace_reader.ml
+++ b/src/core/t_trace_reader.ml
@@ -54,8 +54,12 @@ let decode_term (self : t) ~read_subterm ~tag : Term.t Dec.t =
       Term.app self.tst f a)
   | "Ty" ->
     Dec.(
-      let+ i = int in
-      Term.type_of_univ self.tst i)
+      let* lvl = string in
+      (match int_of_string_opt lvl with
+      | Some i -> return @@ Term.type_of_univ_int self.tst i
+      | None ->
+        (* FIXME: parse/deserialize the level here *)
+        failf "cannot parse level %S" lvl))
   | "Tl" ->
     Dec.(
       let+ v, ty, bod = tup3 string read_subterm read_subterm in
diff --git a/src/core/t_tracer.ml b/src/core/t_tracer.ml
index 33e4f99e..6d77eb70 100644
--- a/src/core/t_tracer.ml
+++ b/src/core/t_tracer.ml
@@ -17,7 +17,9 @@ let emit_term_ (self : state) (t : Term.t) =
         | T.E_var v -> "TV", V.(list [ string (Var.name v); loop' v.v_ty ])
         | T.E_bound_var v -> "Tv", V.(list [ int (Bvar.idx v); loop' v.bv_ty ])
         | T.E_app (f, a) -> "T@", V.(list [ loop' f; loop' a ])
-        | T.E_type i -> "Ty", V.int i
+        | T.E_type lvl ->
+          (* FIXME: actually serialize level *)
+          "Ty", V.string (Level.to_string lvl)
         | T.E_const ({ Const.c_ty; _ } as const) ->
           let tag, view = Const.ser ~ser_t:loop' const in
           ( "Tc",