Nuprl Definition : discrete-function
discrete-function(f) == λI,alpha. (f I alpha I 1)
Definitions occuring in Statement :
nh-id: 1,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
nh-id: 1,
apply: f a,
lambda: λx.A[x]
FDL editor aliases :
discrete-function
Latex:
discrete-function(f) == \mlambda{}I,alpha. (f I alpha I 1)
Date html generated:
2017_02_21-AM-10_45_35
Last ObjectModification:
2017_02_15-PM-00_08_49
Theory : cubical!type!theory
Home
Index