Nuprl Lemma : name-morph-decomp
∀I,J:Cname List. ∀f:name-morph(I;J).
∃L:(Cname × ℕ2) List
∃K:Cname List
(nameset(I) ≡ nameset(map(λp.(fst(p));L) @ K)
∧ (∃g:nameset(K) ⟶ nameset(J)
(Inj(nameset(K);nameset(J);g) ∧ (f = (face-maps-comp(L) o degeneracy-map(g)) ∈ name-morph(I;J)))))
Proof
Definitions occuring in Statement :
face-maps-comp: face-maps-comp(L),
name-comp: (f o g),
degeneracy-map: degeneracy-map(f),
name-morph: name-morph(I;J),
nameset: nameset(L),
coordinate_name: Cname,
map: map(f;as),
append: as @ bs,
list: T List,
inject: Inj(A;B;f),
int_seg: {i..j-},
ext-eq: A ≡ B,
pi1: fst(t),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
lambda: λx.A[x],
function: x:A ⟶ B[x],
product: x:A × B[x],
natural_number: $n,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
nameset: nameset(L),
name-morph: name-morph(I;J),
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
prop: ℙ,
exists: ∃x:A. B[x],
so_lambda: λ2x.t[x],
pi1: fst(t),
subtype_rel: A ⊆r B,
top: Top,
guard: {T},
so_apply: x[s],
mapfilter: mapfilter(f;P;L),
compose: f o g,
ext-eq: A ≡ B,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
bnot: ¬bb,
ifthenelse: if b then t else f fi ,
assert: ↑b,
bfalse: ff,
or: P ∨ Q,
cand: A c∧ B,
true: True,
sq_type: SQType(T),
false: False,
name-morph-domain: name-morph-domain(f;I),
degeneracy-map: degeneracy-map(f),
name-comp: (f o g),
uext: uext(g),
l_subset: l_subset(T;as;bs),
squash: ↓T,
not: ¬A,
int_seg: {i..j-},
l_member: (x ∈ l),
coordinate_name: Cname,
int_upper: {i...},
nat: ℕ,
sq_stable: SqStable(P),
ge: i ≥ j ,
decidable: Dec(P),
satisfiable_int_formula: satisfiable_int_formula(fmla),
outl: outl(x)
Lemmas referenced :
name-morph_wf,
list_wf,
coordinate_name_wf,
mapfilter_wf,
nameset_wf,
list-subtype,
bnot_wf,
isname_wf,
int_seg_wf,
assert_of_bnot,
not-assert-isname,
assert_wf,
exists_wf,
ext-eq_wf,
append_wf,
map_wf,
inject_wf,
equal_wf,
name-comp_wf,
face-maps-comp_wf,
name-morph_subtype,
pi1_wf_top,
subtype_rel_weakening,
degeneracy-map_wf,
map-map,
map-id,
filter_wf_top,
filter_wf5,
l_member_wf,
member_append,
bool_wf,
eqtt_to_assert,
false_wf,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
member_filter_2,
or_wf,
assert-isname,
name-morph-domain-inject,
all_wf,
extd-nameset_wf,
face-maps-comp-property,
nameset_subtype,
ext-eq_inversion,
subtype_rel_transitivity,
squash_wf,
true_wf,
iff_weakening_equal,
set_subtype_base,
lelt_wf,
int_subtype_base,
cname_deq_wf,
strong-subtype-deq-subtype,
strong-subtype-set2,
apply-alist-function,
subtype_rel_list,
top_wf,
le_wf,
select_wf,
sq_stable__le,
nat_properties,
sq_stable__l_member,
decidable__equal-coordinate_name,
decidable__le,
satisfiable-full-omega-tt,
intformand_wf,
intformnot_wf,
intformle_wf,
itermConstant_wf,
itermVar_wf,
int_formula_prop_and_lemma,
int_formula_prop_not_lemma,
int_formula_prop_le_lemma,
int_term_value_constant_lemma,
int_term_value_var_lemma,
int_formula_prop_wf,
less_than_wf,
length_wf,
unit_wf2,
union_subtype_base,
extd-nameset_subtype_base,
unit_subtype_base
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
because_Cache,
equalityTransitivity,
equalitySymmetry,
lambdaEquality,
applyEquality,
setElimination,
rename,
productEquality,
natural_numberEquality,
sqequalRule,
productElimination,
independent_isectElimination,
independent_pairEquality,
setEquality,
dependent_pairFormation,
functionEquality,
functionExtensionality,
isect_memberEquality,
voidElimination,
voidEquality,
independent_pairFormation,
dependent_set_memberEquality,
dependent_functionElimination,
independent_functionElimination,
unionElimination,
equalityElimination,
inrFormation,
promote_hyp,
instantiate,
cumulativity,
inlFormation,
addLevel,
orFunctionality,
imageElimination,
universeEquality,
imageMemberEquality,
baseClosed,
intEquality,
applyLambdaEquality,
int_eqEquality,
computeAll,
unionEquality
Latex:
\mforall{}I,J:Cname List. \mforall{}f:name-morph(I;J).
\mexists{}L:(Cname \mtimes{} \mBbbN{}2) List
\mexists{}K:Cname List
(nameset(I) \mequiv{} nameset(map(\mlambda{}p.(fst(p));L) @ K)
\mwedge{} (\mexists{}g:nameset(K) {}\mrightarrow{} nameset(J)
(Inj(nameset(K);nameset(J);g) \mwedge{} (f = (face-maps-comp(L) o degeneracy-map(g))))))
Date html generated:
2017_10_05-AM-10_10_40
Last ObjectModification:
2017_07_28-AM-11_17_34
Theory : cubical!sets
Home
Index