Nuprl Definition : cubical_context
CubicalContext == X:CubicalSet''' × vs:varname() List × ({v:varname()| (v ∈ vs)} ⟶ cttTerm(X))
Definitions occuring in Statement :
ctt-term-meaning: cttTerm(X),
cubical_set: CubicalSet,
varname: varname(),
l_member: (x ∈ l),
list: T List,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
product: x:A × B[x]
Definitions occuring in definition :
cubical_set: CubicalSet,
product: x:A × B[x],
list: T List,
function: x:A ⟶ B[x],
set: {x:A| B[x]} ,
l_member: (x ∈ l),
varname: varname(),
ctt-term-meaning: cttTerm(X)
FDL editor aliases :
cubical_context
Latex:
CubicalContext == X:CubicalSet''' \mtimes{} vs:varname() List \mtimes{} (\{v:varname()| (v \mmember{} vs)\} {}\mrightarrow{} cttTerm(X))
Date html generated:
2020_05_20-PM-08_01_01
Last ObjectModification:
2020_05_03-PM-05_36_59
Theory : cubical!type!theory
Home
Index