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