Nuprl Definition : ps-canonical-section
ps-canonical-section(Gamma;A;I;rho;a) == λK,f. (a rho f)
Definitions occuring in Statement :
presheaf-type-ap-morph: (u a f),
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
presheaf-type-ap-morph: (u a f)
FDL editor aliases :
ps-canonical-section
Latex:
ps-canonical-section(Gamma;A;I;rho;a) == \mlambda{}K,f. (a rho f)
Date html generated:
2018_05_22-PM-10_04_08
Last ObjectModification:
2018_02_26-PM-05_27_06
Theory : presheaf!models!of!type!theory
Home
Index