Nuprl Rule : uallLevelFunctionality
H x:(∀[x1:T]. P ∈ 𝕌{lvl}), J ⊢ ∀[x2:T]. Q ∈ 𝕌{lvl} ext experimental{uallLevelFunctionality}(Ax)
BY uallLevelFunctionality #$i v w ()
H v:T @lvl, w:P ∈ 𝕌{lvl}[v/x1], J ⊢ Q ∈ 𝕌{lvl}[v/x2]
Definitions occuring in rule :
uall: ∀[x:A]. B[x],
member: t ∈ T,
universe: Type,
axiom: Ax
Latex:
H x:(\mforall{}[x1:T]. P \mmember{} \mBbbU{}\{lvl\}), J \mvdash{} \mforall{}[x2:T]. Q \mmember{} \mBbbU{}\{lvl\} ext experimental\{uallLevelFunctionality\}(Ax)
BY uallLevelFunctionality \#\$i v w ()
H v:T @lvl, w:P \mmember{} \mBbbU{}\{lvl\}[v/x1], J \mvdash{} Q \mmember{} \mBbbU{}\{lvl\}[v/x2]
Date html generated:
2017_09_29-PM-05_44_54
Last ObjectModification:
2016_01_12-PM-01_16_33
Theory : rules
Home
Index