Nuprl Definition : presheaf-fun
(A ⟶ B) == <λI,a. presheaf-fun-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-fun-family: presheaf-fun-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-fun-family: presheaf-fun-family(C; X; A; B; I; a),
lambda: λx.A[x],
apply: f a,
cat-comp: cat-comp(C)
FDL editor aliases :
presheaf-fun
Latex:
(A {}\mrightarrow{} B) == <\mlambda{}I,a. presheaf-fun-family(C; X; A; B; I; a), \mlambda{}I,J,f,a,w,K,g. (w K (cat-comp(C) K J I g\000C f))>
Date html generated:
2018_05_23-AM-08_16_15
Last ObjectModification:
2018_02_21-PM-04_52_23
Theory : presheaf!models!of!type!theory
Home
Index