Nuprl Definition : presheaf-fun-comp
(f o g) == presheaf-lam(G;app((f)p; app((g)p; q)))
Definitions occuring in Statement :
presheaf-app: app(w; u),
presheaf-lam: presheaf-lam(X;b),
psc-snd: q,
psc-fst: p,
pscm-ap-term: (t)s
Definitions occuring in definition :
presheaf-lam: presheaf-lam(X;b),
presheaf-app: app(w; u),
pscm-ap-term: (t)s,
psc-fst: p,
psc-snd: q
FDL editor aliases :
presheaf-fun-comp
Latex:
(f o g) == presheaf-lam(G;app((f)p; app((g)p; q)))
Date html generated:
2018_05_23-AM-08_19_05
Last ObjectModification:
2018_02_21-PM-06_57_28
Theory : presheaf!models!of!type!theory
Home
Index