Nuprl Definition : poset-functor-extends
poset-functor-extends(C;I;L;E;F) ==
(functor-ob(F) = L ∈ (name-morph(I;[]) ⟶ cat-ob(C)))
∧ (∀i:nameset(I). ∀c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} .
((functor-arrow(F) c flip(c;i) (λx.Ax)) = (E i c) ∈ (cat-arrow(C) (L c) (L flip(c;i)))))
Definitions occuring in Statement :
name-morph-flip: flip(f;y),
name-morph: name-morph(I;J),
nameset: nameset(L),
functor-arrow: functor-arrow(F),
functor-ob: functor-ob(F),
cat-arrow: cat-arrow(C),
cat-ob: cat-ob(C),
nil: [],
int_seg: {i..j-},
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
natural_number: $n,
equal: s = t ∈ T,
axiom: Ax
Definitions occuring in definition :
and: P ∧ Q,
function: x:A ⟶ B[x],
cat-ob: cat-ob(C),
functor-ob: functor-ob(F),
nameset: nameset(L),
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
name-morph: name-morph(I;J),
nil: [],
int_seg: {i..j-},
natural_number: $n,
equal: s = t ∈ T,
cat-arrow: cat-arrow(C),
functor-arrow: functor-arrow(F),
name-morph-flip: flip(f;y),
lambda: λx.A[x],
axiom: Ax,
apply: f a
FDL editor aliases :
poset-functor-extends
Latex:
poset-functor-extends(C;I;L;E;F) ==
(functor-ob(F) = L)
\mwedge{} (\mforall{}i:nameset(I). \mforall{}c:\{c:name-morph(I;[])| (c i) = 0\} .
((functor-arrow(F) c flip(c;i) (\mlambda{}x.Ax)) = (E i c)))
Date html generated:
2016_06_16-PM-06_57_30
Last ObjectModification:
2015_09_23-AM-09_33_07
Theory : cubical!sets
Home
Index