Nuprl Definition : presheaf-sigma-fun
presheaf-sigma-fun(G;A;B;f) == presheaf-lam(G;presheaf-pair(q.1;app(app(((λf))p; q.1); q.2)))
Definitions occuring in Statement :
presheaf-pair: presheaf-pair(u;v),
presheaf-snd: p.2,
presheaf-fst: p.1,
presheaf-app: app(w; u),
presheaf-lam: presheaf-lam(X;b),
presheaf-lambda: (λb),
psc-snd: q,
psc-fst: p,
pscm-ap-term: (t)s
Definitions occuring in definition :
presheaf-lam: presheaf-lam(X;b),
presheaf-pair: presheaf-pair(u;v),
presheaf-app: app(w; u),
pscm-ap-term: (t)s,
psc-fst: p,
presheaf-lambda: (λb),
presheaf-fst: p.1,
presheaf-snd: p.2,
psc-snd: q
FDL editor aliases :
presheaf-sigma-fun
Latex:
presheaf-sigma-fun(G;A;B;f) == presheaf-lam(G;presheaf-pair(q.1;app(app(((\mlambda{}f))p; q.1); q.2)))
Date html generated:
2018_05_23-AM-08_23_46
Last ObjectModification:
2018_02_21-PM-11_31_51
Theory : presheaf!models!of!type!theory
Home
Index