### 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