Nuprl Definition : dual-plane-primitives
DualPlanePrimitives ==  "V":Type"S":self."V" ⟶ self."V" ⟶ ℙ"P":self."V" ⟶ self."V" ⟶ ℙ
Definitions occuring in Statement : 
record-select: r.x
, 
record+: record+, 
record: record(x.T[x])
, 
top: Top
, 
prop: ℙ
, 
function: x:A ⟶ B[x]
, 
token: "$token"
, 
universe: Type
Definitions occuring in definition : 
prop: ℙ
, 
token: "$token"
, 
record-select: r.x
, 
function: x:A ⟶ B[x]
, 
universe: Type
, 
top: Top
, 
record: record(x.T[x])
, 
record+: record+
FDL editor aliases : 
dual-plane-primitives
Latex:
DualPlanePrimitives  ==    "V":Type"S":self."V"  {}\mrightarrow{}  self."V"  {}\mrightarrow{}  \mBbbP{}"P":self."V"  {}\mrightarrow{}  self."V"  {}\mrightarrow{}  \mBbbP{}
Date html generated:
2018_05_21-PM-09_44_20
Last ObjectModification:
2018_05_09-AM-11_24_34
Theory : matrices
Home
Index