Nuprl Definition : presheaf-fun-family
presheaf-fun-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))|
∀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) g) = (w K (cat-comp(C) K J I g f) (u f(a) g)) ∈ B(g(f(a))))}
Definitions occuring in Statement :
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),
apply: f a,
cat-comp: cat-comp(C),
presheaf-type-ap-morph: (u a f),
psc-restriction: f(s)
Latex:
presheaf-fun-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))|
\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) g) = (w K (cat-comp(C) K J I g f) (u f(a) g)))\}
Date html generated:
2018_05_23-AM-08_15_22
Last ObjectModification:
2018_02_21-PM-03_36_29
Theory : presheaf!models!of!type!theory
Home
Index