Nuprl Definition : presheaf-pi-family
presheaf-pi-family(C; X; A; B; I; a) ==
{w:J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A(f(a)) ⟶ B((f(a);u))|
∀J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀u:A(f(a)).
((w J f u (f(a);u) g) = (w K (cat-comp(C) K J I g f) (u f(a) g)) ∈ B(g((f(a);u))))}
Definitions occuring in Statement :
psc-adjoin-set: (v;u),
psc-adjoin: X.A,
presheaf-type-ap-morph: (u a f),
presheaf-type-at: A(a),
psc-restriction: f(s),
cat-comp: cat-comp(C),
cat-arrow: cat-arrow(C),
cat-ob: cat-ob(C),
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
cat-ob: cat-ob(C),
cat-arrow: cat-arrow(C),
all: ∀x:A. B[x],
equal: s = t ∈ T,
presheaf-type-at: A(a),
psc-adjoin: X.A,
psc-adjoin-set: (v;u),
apply: f a,
cat-comp: cat-comp(C),
presheaf-type-ap-morph: (u a f),
psc-restriction: f(s)
FDL editor aliases :
presheaf-pi-family
Latex:
presheaf-pi-family(C; X; A; B; I; a) ==
\{w:J:cat-ob(C) {}\mrightarrow{} f:(cat-arrow(C) J I) {}\mrightarrow{} u:A(f(a)) {}\mrightarrow{} B((f(a);u))|
\mforall{}J,K:cat-ob(C). \mforall{}f:cat-arrow(C) J I. \mforall{}g:cat-arrow(C) K J. \mforall{}u:A(f(a)).
((w J f u (f(a);u) g) = (w K (cat-comp(C) K J I g f) (u f(a) g)))\}
Date html generated:
2018_05_23-AM-08_14_41
Last ObjectModification:
2018_02_21-PM-02_26_44
Theory : presheaf!models!of!type!theory
Home
Index