Inductive Empty@{uu} : Type@{uu} :=  .
(* uu |=  *)
Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap
  { punwrap : A }.
(* uu |=  *)

PWrap has primitive projections with eta conversion.
Arguments PWrap _%type_scope
Arguments pwrap _%type_scope _
punwrap@{uu} = 
fun (A : Type@{uu}) (p : PWrap@{uu} A) => punwrap _ p
     : forall A : Type@{uu}, PWrap@{uu} A -> A
(* uu |=  *)

Arguments punwrap _%type_scope _
Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap
  { runwrap : A }.
(* uu |=  *)

Arguments RWrap _%type_scope
Arguments rwrap _%type_scope _
runwrap@{uu} = 
fun (A : Type@{uu}) (r : RWrap@{uu} A) => let (runwrap) := r in runwrap
     : forall A : Type@{uu}, RWrap@{uu} A -> A
(* uu |=  *)

Arguments runwrap _%type_scope _
Wrap@{uu} = fun A : Type@{uu} => A
     : Type@{uu} -> Type@{uu}
(* uu |=  *)

Arguments Wrap _%type_scope
wrap@{uu} = 
fun (A : Type@{uu}) (Wrap : Wrap@{uu} A) => Wrap
     : forall A : Type@{uu}, Wrap@{uu} A -> A
(* uu |=  *)

Arguments wrap {A}%type_scope {Wrap}
bar@{uu} = nat
     : Wrap@{uu} Set
(* uu |= Set < uu *)
foo@{uu u v} = 
Type@{u} -> Type@{v} -> Type@{uu}
     : Type@{max(uu+1,u+1,v+1)}
(* uu u v |=  *)
Type@{i} -> Type@{j}
     : Type@{max(i+1,j+1)}
(* {j i} |=  *)
     = Type@{i} -> Type@{j}
     : Type@{max(i+1,j+1)}
(* {j i} |=  *)
mono = Type@{mono.uu}
     : Type@{mono.uu+1}
(* {mono.uu} |=  *)
mono
     : Type@{mono.uu+1}
Type@{mono.uu}
     : Type@{mono.uu+1}
The command has indeed failed with message:
Universe uu already exists.
monomono
     : Type@{MONOU+1}
mono.monomono
     : Type@{mono.MONOU+1}
monomono
     : Type@{MONOU+1}
mono
     : Type@{mono.uu+1}
The command has indeed failed with message:
Universe uu already exists.
bobmorane = 
let tt := Type@{UnivBinders.32} in
let ff := Type@{UnivBinders.34} in tt -> ff
     : Type@{max(UnivBinders.31,UnivBinders.33)}
The command has indeed failed with message:
Universe uu already bound.
foo@{E M N} = 
Type@{M} -> Type@{N} -> Type@{E}
     : Type@{max(E+1,M+1,N+1)}
(* E M N |=  *)
foo@{uu u v} = 
Type@{u} -> Type@{v} -> Type@{uu}
     : Type@{max(uu+1,u+1,v+1)}
(* uu u v |=  *)
Inductive Empty@{E} : Type@{E} :=  .
(* E |=  *)
Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }.
(* E |=  *)

PWrap has primitive projections with eta conversion.
Arguments PWrap _%type_scope
Arguments pwrap _%type_scope _
punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A
(* K |=  *)

punwrap is universe polymorphic
Arguments punwrap _%type_scope _
punwrap is transparent
Expands to: Constant UnivBinders.punwrap
The command has indeed failed with message:
Universe instance should have length 3
The command has indeed failed with message:
Universe instance should have length 0
The command has indeed failed with message:
This object does not support universe names.
The command has indeed failed with message:
Cannot enforce v < u because u < gU < gV < v
insec@{v} = Type@{uu} -> Type@{v}
     : Type@{max(uu+1,v+1)}
(* v |=  *)
Inductive insecind@{k} : Type@{k+1} :=
    inseccstr : Type@{k} -> insecind@{k}.
(* k |=  *)

Arguments inseccstr _%type_scope
insec@{uu v} = Type@{uu} -> Type@{v}
     : Type@{max(uu+1,v+1)}
(* uu v |=  *)
Inductive insecind@{uu k} : Type@{k+1} :=
    inseccstr : Type@{k} -> insecind@{uu k}.
(* uu k |=  *)

Arguments inseccstr _%type_scope
insec2@{u} = Prop
     : Type@{Set+1}
(* u |=  *)
inmod@{uu} = Type@{uu}
     : Type@{uu+1}
(* uu |=  *)
SomeMod.inmod@{uu} = Type@{uu}
     : Type@{uu+1}
(* uu |=  *)
inmod@{uu} = Type@{uu}
     : Type@{uu+1}
(* uu |=  *)
Applied.infunct@{uu v} = 
inmod@{uu} -> Type@{v}
     : Type@{max(uu+1,v+1)}
(* uu v |=  *)
axfoo@{i u u0} : Type@{u} -> Type@{i}
(* i u u0 |=  *)

axfoo is universe polymorphic
Arguments axfoo _%type_scope
Expands to: Constant UnivBinders.axfoo
axbar@{i u u0} : Type@{u0} -> Type@{i}
(* i u u0 |=  *)

axbar is universe polymorphic
Arguments axbar _%type_scope
Expands to: Constant UnivBinders.axbar
axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i}

axfoo' is not universe polymorphic
Arguments axfoo' _%type_scope
Expands to: Constant UnivBinders.axfoo'
axbar' : Type@{axfoo'.u0} -> Type@{axfoo'.i}

axbar' is not universe polymorphic
Arguments axbar' _%type_scope
Expands to: Constant UnivBinders.axbar'
The command has indeed failed with message:
When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block).
foo@{i} = Type@{M.i} -> Type@{i}
     : Type@{max(M.i+1,i+1)}
(* i |=  *)
Type@{u0} -> Type@{UnivBinders.64}
     : Type@{max(u0+1,UnivBinders.64+1)}
(* {UnivBinders.64} |=  *)
bind_univs.mono = 
Type@{bind_univs.mono.u}
     : Type@{bind_univs.mono.u+1}
(* {bind_univs.mono.u} |=  *)
bind_univs.poly@{u} = Type@{u}
     : Type@{u+1}
(* u |=  *)