Nuprl Definition : csm-m
m == λI,c. let a,s = c in let rho,r = a in (rho;r ∧ s)
Definitions occuring in Statement :
cc-adjoin-cube: (v;u),
dM: dM(I),
lattice-meet: a ∧ b,
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
lambda: λx.A[x],
spread: spread def,
cc-adjoin-cube: (v;u),
lattice-meet: a ∧ b,
dM: dM(I)
FDL editor aliases :
csm-m
Latex:
m == \mlambda{}I,c. let a,s = c in let rho,r = a in (rho;r \mwedge{} s)
Date html generated:
2016_05_19-AM-10_44_46
Last ObjectModification:
2016_04_04-PM-03_14_59
Theory : cubical!type!theory
Home
Index