Nuprl Lemma : unique-poset-functor
∀C:SmallCategory. ∀I:Cname List. ∀L:name-morph(I;[]) ⟶ cat-ob(C). ∀E:i:nameset(I)
⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2}
⟶ (cat-arrow(C) (L c) (L flip(c;i))).
(edge-arrows-commute(C;I;L;E) ⇒ (∃!F:Functor(poset-cat(I);C). poset-functor-extends(C;I;L;E;F)))
Proof
Definitions occuring in Statement :
edge-arrows-commute: edge-arrows-commute(C;I;L;E),
poset-functor-extends: poset-functor-extends(C;I;L;E;F),
poset-cat: poset-cat(J),
name-morph-flip: flip(f;y),
name-morph: name-morph(I;J),
nameset: nameset(L),
coordinate_name: Cname,
cat-functor: Functor(C1;C2),
cat-arrow: cat-arrow(C),
cat-ob: cat-ob(C),
small-category: SmallCategory,
nil: [],
list: T List,
int_seg: {i..j-},
exists!: ∃!x:T. P[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ,
uall: ∀[x:A]. B[x],
name-morph: name-morph(I;J),
subtype_rel: A ⊆r B,
uimplies: b supposing a,
exists!: ∃!x:T. P[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
cand: A c∧ B,
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
poset-extend-unique,
equal_wf,
all_wf,
and_wf,
poset-cat_wf,
cat-functor_wf,
poset-functor-extends_wf,
poset_functor_extend-extends,
poset_functor_extend-is-functor,
small-category_wf,
list_wf,
cat-ob_wf,
name-morph-flip_wf,
cat-arrow_wf,
int_seg_wf,
equal-wf-T-base,
coordinate_name_wf,
nil_wf,
name-morph_wf,
nameset_wf,
edge-arrows-commute_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
hypothesis,
functionEquality,
isectElimination,
setEquality,
because_Cache,
natural_numberEquality,
applyEquality,
setElimination,
rename,
sqequalRule,
baseClosed,
independent_isectElimination,
equalityTransitivity,
equalitySymmetry,
dependent_pairFormation,
independent_pairFormation,
lambdaEquality
Latex:
\mforall{}C:SmallCategory. \mforall{}I:Cname List. \mforall{}L:name-morph(I;[]) {}\mrightarrow{} cat-ob(C). \mforall{}E:i:nameset(I)
{}\mrightarrow{} c:\{c:name-morph(I;[])|
(c i) = 0\}
{}\mrightarrow{} (cat-arrow(C) (L c)
(L flip(c;i))).
(edge-arrows-commute(C;I;L;E) {}\mRightarrow{} (\mexists{}!F:Functor(poset-cat(I);C). poset-functor-extends(C;I;L;E;F)))
Date html generated:
2016_06_16-PM-07_01_33
Last ObjectModification:
2016_01_18-PM-04_48_59
Theory : cubical!sets
Home
Index