Nuprl Definition : presheaf-pi
ΠA B == <λI,a. presheaf-pi-family(C; X; A; B; I; a), λI,J,f,a,w,K,g. (w K (cat-comp(C) K J I g f))>
Definitions occuring in Statement :
presheaf-pi-family: presheaf-pi-family(C; X; A; B; I; a),
cat-comp: cat-comp(C),
apply: f a,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
presheaf-pi-family: presheaf-pi-family(C; X; A; B; I; a),
lambda: λx.A[x],
apply: f a,
cat-comp: cat-comp(C)
FDL editor aliases :
presheaf-pi
Latex:
\mPi{}A B == <\mlambda{}I,a. presheaf-pi-family(C; X; A; B; I; a), \mlambda{}I,J,f,a,w,K,g. (w K (cat-comp(C) K J I g f))>
Date html generated:
2018_05_23-AM-08_15_37
Last ObjectModification:
2018_02_21-PM-02_26_49
Theory : presheaf!models!of!type!theory
Home
Index