Nuprl Definition : candidate-type-system
candidate-type-system{i:l,j:l}(Term) == Term ⟶ Term ⟶ term-equality{i:l}(Term) ⟶ 𝕌{j}
Definitions occuring in Statement :
term-equality: term-equality{i:l}(Term),
function: x:A ⟶ B[x],
universe: Type
Definitions occuring in definition :
function: x:A ⟶ B[x],
term-equality: term-equality{i:l}(Term),
universe: Type
FDL editor aliases :
candidate-type-system
Latex:
candidate-type-system\{i:l,j:l\}(Term) == Term {}\mrightarrow{} Term {}\mrightarrow{} term-equality\{i:l\}(Term) {}\mrightarrow{} \mBbbU{}\{j\}
Date html generated:
2016_05_15-PM-01_49_06
Last ObjectModification:
2015_09_23-AM-07_37_15
Theory : parameterized!rec
Home
Index