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

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

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

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

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

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

Arguments wrap {A}%type_scope {Wrap}
bar@{u} = nat
     : Wrap@{u} Set
(* u |= Set < u *)
foo@{u UnivBinders.18 v} = 
Type@{UnivBinders.18} -> Type@{v} -> Type@{u}
     : Type@{max(u+1,UnivBinders.18+1,v+1)}
(* u UnivBinders.18 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.u}
     : Type@{mono.u+1}
(* {mono.u} |=  *)
mono
     : Type@{mono.u+1}
Type@{mono.u}
     : Type@{mono.u+1}
The command has indeed failed with message:
Universe u already exists.
monomono
     : Type@{MONOU+1}
mono.monomono
     : Type@{mono.MONOU+1}
monomono
     : Type@{MONOU+1}
mono
     : Type@{mono.u+1}
The command has indeed failed with message:
Universe u already exists.
bobmorane = 
let tt := Type@{UnivBinders.33} in
let ff := Type@{UnivBinders.35} in tt -> ff
     : Type@{max(UnivBinders.32,UnivBinders.34)}
The command has indeed failed with message:
Universe u already bound.
foo@{E M N} = 
Type@{M} -> Type@{N} -> Type@{E}
     : Type@{max(E+1,M+1,N+1)}
(* E M N |=  *)
foo@{u UnivBinders.18 v} = 
Type@{UnivBinders.18} -> Type@{v} -> Type@{u}
     : Type@{max(u+1,UnivBinders.18+1,v+1)}
(* u UnivBinders.18 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
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 |=  *)
insec@{v} = Type@{u} -> Type@{v}
     : Type@{max(u+1,v+1)}
(* v |=  *)
Inductive insecind@{k} : Type@{k+1} :=
    inseccstr : Type@{k} -> insecind@{k}
(* k |=  *)

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

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

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

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).