Nuprl Lemma : poset_functor_extend_same

∀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))).
∀x:cat-ob(poset-cat(I)).
  ∀[y:cat-ob(poset-cat(I))]
    poset_functor_extend(C;I;L;E;x;y) = (cat-id(C) (L x)) ∈ (cat-arrow(C) (L x) (L x)) 
    supposing x = y ∈ cat-ob(poset-cat(I))


Proof



Definitions occuring in Statement :  poset_functor_extend: poset_functor_extend(C;I;L;E;c1;c2),  poset-cat: poset-cat(J),  name-morph-flip: flip(f;y),  name-morph: name-morph(I;J),  nameset: nameset(L),  coordinate_name: Cname,  cat-id: cat-id(C),  cat-arrow: cat-arrow(C),  cat-ob: cat-ob(C),  small-category: SmallCategory,  nil: [],  list: T List,  int_seg: {i..j-},  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  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],  uall: ∀[x:A]. B[x],  member: t ∈ T,  uimplies: b supposing a,  squash: ↓T,  prop: ℙ,  subtype_rel: A ⊆r B,  cat-ob: cat-ob(C),  pi1: fst(t),  poset-cat: poset-cat(J),  name-morph: name-morph(I;J),  so_lambda: λ2x.t[x],  so_apply: x[s],  and: P ∧ Q,  implies: P ⇒ Q,  true: True,  guard: {T},  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q
Lemmas referenced :  equal_wf,  squash_wf,  true_wf,  cat-arrow_wf,  subtype_rel_self,  name-morph_wf,  nil_wf,  coordinate_name_wf,  poset_functor_extend_wf,  all_wf,  nameset_wf,  le_wf,  extd-nameset_subtype_int,  set_wf,  equal-wf-T-base,  int_seg_wf,  extd-nameset-nil,  name-morph-flip_wf,  cat-ob_wf,  list_wf,  small-category_wf,  le_reflexive,  and_wf,  poset-cat_wf,  extd-nameset_wf,  assert_wf,  isname_wf,  subtype_rel_wf,  cat-id_wf,  iff_weakening_equal,  poset_functor_extend_id
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  lambdaFormation,  isect_memberFormation,  introduction,  cut,  applyEquality,  thin,  lambdaEquality,  sqequalHypSubstitution,  imageElimination,  extract_by_obid,  isectElimination,  hypothesisEquality,  equalityTransitivity,  hypothesis,  equalitySymmetry,  universeEquality,  functionExtensionality,  because_Cache,  sqequalRule,  independent_isectElimination,  setElimination,  rename,  functionEquality,  natural_numberEquality,  baseClosed,  dependent_functionElimination,  hyp_replacement,  dependent_set_memberEquality,  independent_pairFormation,  applyLambdaEquality,  productElimination,  setEquality,  imageMemberEquality,  independent_functionElimination,  isect_memberEquality,  axiomEquality
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))).
\mforall{}x:cat-ob(poset-cat(I)).
    \mforall{}[y:cat-ob(poset-cat(I))].  poset\_functor\_extend(C;I;L;E;x;y)  =  (cat-id(C)  (L  x))  supposing  x  =  y


Date html generated: 2017_10_05-AM-10_30_57
Last ObjectModification: 2017_07_28-AM-11_24_37

Theory : cubical!sets


Home Index