Nuprl Lemma : poset_functor_extend-flip
∀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))).
∀i:nameset(I). ∀c:cat-ob(poset-cat(I)).
poset_functor_extend(C;I;L;E;c;flip(c;i)) = (E i c) ∈ (cat-arrow(C) (L c) (L flip(c;i))) supposing (c i) = 0 ∈ ℕ2
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-arrow: cat-arrow(C),
cat-ob: cat-ob(C),
small-category: SmallCategory,
nil: [],
list: T List,
int_seg: {i..j-},
uimplies: b supposing a,
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],
member: t ∈ T,
uimplies: b supposing a,
poset-functor-extends: poset-functor-extends(C;I;L;E;F),
and: P ∧ Q,
functor-arrow: functor-arrow(F),
pi2: snd(t),
subtype_rel: A ⊆r B,
cat-ob: cat-ob(C),
pi1: fst(t),
poset-cat: poset-cat(J),
name-morph: name-morph(I;J),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_lambda: λ2x.t[x],
implies: P ⇒ Q,
so_apply: x[s]
Lemmas referenced :
small-category_wf,
list_wf,
name-morph-flip_wf,
cat-arrow_wf,
set_wf,
poset-cat_wf,
cat-ob_wf,
equal_wf,
isname_wf,
assert_wf,
all_wf,
extd-nameset_wf,
nameset_wf,
int_seg_wf,
equal-wf-T-base,
coordinate_name_wf,
nil_wf,
name-morph_wf,
subtype_rel_self,
poset_functor_extend-extends
Rules used in proof :
cut,
lemma_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
isect_memberFormation,
productElimination,
sqequalRule,
dependent_set_memberEquality,
applyEquality,
isectElimination,
natural_numberEquality,
setElimination,
rename,
because_Cache,
baseClosed,
lambdaEquality,
setEquality,
functionEquality
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{}i:nameset(I). \mforall{}c:cat-ob(poset-cat(I)).
poset\_functor\_extend(C;I;L;E;c;flip(c;i)) = (E i c) supposing (c i) = 0
Date html generated:
2016_06_16-PM-06_58_00
Last ObjectModification:
2016_01_18-PM-04_49_28
Theory : cubical!sets
Home
Index