Nuprl Definition : presheaf-term
{X ⊢ _:A} ==
{u:I:cat-ob(C) ⟶ a:X(I) ⟶ A(a)|
∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I). ((u I a a f) = (u J f(a)) ∈ A(f(a)))}
Definitions occuring in Statement :
presheaf-type-ap-morph: (u a f),
presheaf-type-at: A(a),
psc-restriction: f(s),
I_set: A(I),
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],
I_set: A(I),
equal: s = t ∈ T,
presheaf-type-at: A(a),
presheaf-type-ap-morph: (u a f),
apply: f a,
psc-restriction: f(s)
FDL editor aliases :
presheaf-term
Latex:
\{X \mvdash{} \_:A\} ==
\{u:I:cat-ob(C) {}\mrightarrow{} a:X(I) {}\mrightarrow{} A(a)|
\mforall{}I,J:cat-ob(C). \mforall{}f:cat-arrow(C) J I. \mforall{}a:X(I). ((u I a a f) = (u J f(a)))\}
Date html generated:
2018_05_22-PM-10_03_50
Last ObjectModification:
2018_02_21-AM-11_52_56
Theory : presheaf!models!of!type!theory
Home
Index