Nuprl Definition : ctt-meaning-triple
CttMeaningTriple == X:?CubicalContext × bt:varname() List × CttTerm × [[X;snd(bt)]]
Definitions occuring in Statement :
ctt_meaning: [[ctxt;t]],
ctt-term: CttTerm,
cubical-context: ?CubicalContext,
varname: varname(),
list: T List,
pi2: snd(t),
product: x:A × B[x]
Definitions occuring in definition :
cubical-context: ?CubicalContext,
product: x:A × B[x],
list: T List,
varname: varname(),
ctt-term: CttTerm,
ctt_meaning: [[ctxt;t]],
pi2: snd(t)
FDL editor aliases :
ctt-meaning-triple
Latex:
CttMeaningTriple == X:?CubicalContext \mtimes{} bt:varname() List \mtimes{} CttTerm \mtimes{} [[X;snd(bt)]]
Date html generated:
2020_05_21-AM-10_34_01
Last ObjectModification:
2020_03_12-PM-01_31_12
Theory : cubical!type!theory
Home
Index