Things which don't mention `Type` explicitly usually don't change the type level.  If I `Set Printing Universes` on my version (which has slightly different names), I get
```coq
Record PreCategory
    : Type
      (* max(HoTT.Categories.Category.Core.30+1, HoTT.Categories.Category.Core.31+1) *)
  := Build_PreCategory'
  { Object : Type (* HoTT.Categories.Category.Core.30 *);
    Morphism : Object ->
               Object -> Type (* HoTT.Categories.Category.Core.31 *);
    Identity : forall x : Object, Morphism x x;
    Compose : forall s d d' : Object,
              Morphism d d' -> Morphism s d -> Morphism s d';
    Associativity : forall (x1 x2 x3 x4 : Object) (m1 : Morphism x1 x2)
                      (m2 : Morphism x2 x3) (m3 : Morphism x3 x4),
                    Compose x1 x2 x4 (Compose x2 x3 x4 m3 m2) m1 =
                    Compose x1 x3 x4 m3 (Compose x1 x2 x3 m2 m1);
    Associativity_sym : forall (x1 x2 x3 x4 : Object)
                          (m1 : Morphism x1 x2) (m2 : Morphism x2 x3)
                          (m3 : Morphism x3 x4),
                        Compose x1 x3 x4 m3 (Compose x1 x2 x3 m2 m1) =
                        Compose x1 x2 x4 (Compose x2 x3 x4 m3 m2) m1;
    LeftIdentity : forall (a b : Object) (f : Morphism a b),
                   Compose a b b (Identity b) f = f;
    RightIdentity : forall (a b : Object) (f : Morphism a b),
                    Compose a a b f (Identity a) = f;
    IdentityIdentity : forall x : Object,
                       Compose x x x (Identity x) (Identity x) = Identity x;
    MorphismIsHSet : forall s d : Object,
                     IsTrunc (* HoTT.Categories.Category.Core.31 *) 0
                       (Morphism s d) }
(* HoTT.Categories.Category.Core.30
   HoTT.Categories.Category.Core.31 |=  *)
```