Nuprl Definition : discrete-fun
discrete-fun(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-fun
Latex:
discrete-fun(f) == \mlambda{}I,alpha. (f I alpha I 1)
Date html generated:
2017_02_21-AM-10_42_48
Last ObjectModification:
2017_02_10-PM-11_14_08
Theory : cubical!type!theory
Home
Index