Nuprl Definition : presheaf-type
{X ⊢ _} ==
{AF:A:I:cat-ob(C) ⟶ X(I) ⟶ Type × (I:cat-ob(C)
⟶ J:cat-ob(C)
⟶ f:(cat-arrow(C) J I)
⟶ a:X(I)
⟶ (A I a)
⟶ (A J f(a)))|
let A,F = AF
in (∀I:cat-ob(C). ∀a:X(I). ∀u:A I a. ((F I I (cat-id(C) I) a u) = u ∈ (A I a)))
∧ (∀I,J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀a:X(I). ∀u:A I a.
((F I K (cat-comp(C) K J I g f) a u) = (F J K g f(a) (F I J f a u)) ∈ (A K cat-comp(C) K J I g f(a))))}
Definitions occuring in Statement :
psc-restriction: f(s),
I_set: A(I),
cat-comp: cat-comp(C),
cat-id: cat-id(C),
cat-arrow: cat-arrow(C),
cat-ob: cat-ob(C),
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
spread: spread def,
product: x:A × B[x],
universe: Type,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
product: x:A × B[x],
universe: Type,
function: x:A ⟶ B[x],
spread: spread def,
and: P ∧ Q,
cat-id: cat-id(C),
cat-ob: cat-ob(C),
cat-arrow: cat-arrow(C),
I_set: A(I),
all: ∀x:A. B[x],
equal: s = t ∈ T,
cat-comp: cat-comp(C),
psc-restriction: f(s),
apply: f a
FDL editor aliases :
presheaf-type
Latex:
\{X \mvdash{} \_\} ==
\{AF:A:I:cat-ob(C) {}\mrightarrow{} X(I) {}\mrightarrow{} Type \mtimes{} (I:cat-ob(C)
{}\mrightarrow{} J:cat-ob(C)
{}\mrightarrow{} f:(cat-arrow(C) J I)
{}\mrightarrow{} a:X(I)
{}\mrightarrow{} (A I a)
{}\mrightarrow{} (A J f(a)))|
let A,F = AF
in (\mforall{}I:cat-ob(C). \mforall{}a:X(I). \mforall{}u:A I a. ((F I I (cat-id(C) I) a u) = u))
\mwedge{} (\mforall{}I,J,K:cat-ob(C). \mforall{}f:cat-arrow(C) J I. \mforall{}g:cat-arrow(C) K J. \mforall{}a:X(I). \mforall{}u:A I a.
((F I K (cat-comp(C) K J I g f) a u) = (F J K g f(a) (F I J f a u))))\}
Date html generated:
2018_05_22-PM-10_01_38
Last ObjectModification:
2018_02_20-PM-03_14_10
Theory : presheaf!models!of!type!theory
Home
Index