Nuprl Definition : discrete-unary
discrete-unary(t;x.f[x]) == λI,a. f[t(a)]
Definitions occuring in Statement :
presheaf-term-at: u(a),
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
presheaf-term-at: u(a)
FDL editor aliases :
discrete-unary
discrete-unary
Latex:
discrete-unary(t;x.f[x]) == \mlambda{}I,a. f[t(a)]
Date html generated:
2018_05_23-AM-08_24_17
Last ObjectModification:
2018_02_21-PM-11_15_20
Theory : presheaf!models!of!type!theory
Home
Index