Nuprl Definition : constant-presheaf-type
(X) == <λI,alpha. X(I), λI,J,f,alpha,w. f(w)>
Definitions occuring in Statement :
psc-restriction: f(s),
I_set: A(I),
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
I_set: A(I),
lambda: λx.A[x],
psc-restriction: f(s)
FDL editor aliases :
constant-presheaf-type
Latex:
(X) == <\mlambda{}I,alpha. X(I), \mlambda{}I,J,f,alpha,w. f(w)>
Date html generated:
2018_05_23-AM-08_25_07
Last ObjectModification:
2018_02_21-PM-11_40_30
Theory : presheaf!models!of!type!theory
Home
Index