Nuprl Definition : universe def
Type == PRIMITIVE
Rules referencing :
imageEquality,
universeEquality,
atomEquality,
voidEquality,
intEquality,
unionEquality,
inlFormation,
inrFormation,
inlEquality,
inrEquality,
functionEquality,
lambdaFormation,
lambdaEquality,
functionUniverseElim,
functionExtensionality,
productEquality,
dependent_pairFormation,
dependent_pairEquality,
productUniverseElim,
setEquality,
dependent_set_memberFormation,
dependent_set_memberEquality,
equalityUniverse,
equalityEquality,
equalityEqualityBase,
baseEquality,
levelHypothesis,
addLevel,
pointwiseFunctionalityForEquality,
substitution,
hyp_replacement,
cumulativity,
barInduction,
bar_Induction,
strong_bar_Induction,
isectEquality,
isect_memberFormation,
isect_memberEquality,
classicalIntroduction,
pointwiseFunctionality,
pointwiseFunctionality wrename,
sqntypeEquality,
sqntypeIntro,
sqequalExtensionalEquality,
sqequalIntensionalEquality,
sqleExtensionalEquality,
sqleIntensionalEquality,
sqlenIntensionalEquality,
sqequalnIntensionalEquality,
atomnEquality,
freeFromAtomEquality,
callbyvalueType,
pertypeEquality,
pertypeMemberEquality,
pertypeElimination,
perfunctionExtensionality,
dependentIntersectionEquality,
existsFunctionality,
allLevelFunctionality,
uallLevelFunctionality,
existsLevelFunctionality,
andLevelFunctionality,
orLevelFunctionality,
orFunctionality,
impliesFunctionality,
impliesLevelFunctionality
FDL editor aliases :
univ
Latex:
Type == PRIMITIVE
Date html generated:
2016_05_13-PM-03_03_37
Last ObjectModification:
2006_01_26-PM-03_51_57
Theory : core_1
Home
Index