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