### Nuprl Lemma : name-morph-extend-face-map

`∀[I,K:Cname List]. ∀[i:ℕ2]. ∀[f:name-morph(I;K)].`
`  (((fresh-cname(I):=i) o f) = ((f)+ o (fresh-cname(K):=i)) ∈ name-morph(I+;K))`

Proof

Definitions occuring in Statement :  name-comp: `(f o g)` face-map: `(x:=i)` name-morph-extend: `(f)+` name-morph: `name-morph(I;J)` add-fresh-cname: `I+` fresh-cname: `fresh-cname(I)` coordinate_name: `Cname` list: `T List` int_seg: `{i..j-}` uall: `∀[x:A]. B[x]` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` name-morph: `name-morph(I;J)` uimplies: `b supposing a` name-morph-extend: `(f)+` name-comp: `(f o g)` has-value: `(a)↓` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` eq-cname: `eq-cname(x;y)` compose: `f o g` nameset: `nameset(L)` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` coordinate_name: `Cname` int_upper: `{i...}` int_seg: `{i..j-}` lelt: `i ≤ j < k` less_than: `a < b` squash: `↓T` face-map: `(x:=i)` uext: `uext(g)` isname: `isname(z)` le: `A ≤ B` satisfiable_int_formula: `satisfiable_int_formula(fmla)` true: `True` nequal: `a ≠ b ∈ T ` top: `Top` add-fresh-cname: `I+`
Lemmas referenced :  name-morphs-equal add-fresh-cname_wf name-comp_wf face-map_wf_fresh-cname name-morph-extend_wf value-type-has-value coordinate_name_wf not_wf l_member_wf set-value-type coordinate_name-value-type fresh-cname_wf eq-cname_wf eqtt_to_assert assert-eq-cname eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot iff_weakening_uiff assert_wf equal_wf nameset_wf name-morph_wf int_seg_wf set_subtype_base le_wf istype-int int_subtype_base eq_int_wf assert_of_eq_int bool_wf iff_imp_equal_bool le_int_wf bfalse_wf iff_functionality_wrt_iff false_wf assert_of_le_int iff_weakening_equal int_seg_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf istype-le istype-void isname-name nsub2_subtype_extd-nameset assert_elim bnot_wf eq_int_eq_true btrue_neq_bfalse neg_assert_of_eq_int btrue_wf not_assert_elim intformnot_wf intformeq_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma squash_wf true_wf istype-universe subtype_rel_self istype-true cons_member assert-isname nameset_subtype_extd-nameset isname_wf extd-nameset_subtype_int equal-wf-T-base uiff_transitivity assert_of_bnot fresh-cname-not-member
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality lambdaEquality_alt setElimination rename inhabitedIsType equalityTransitivity equalitySymmetry sqequalRule independent_isectElimination callbyvalueReduce setEquality universeIsType because_Cache lambdaFormation_alt unionElimination equalityElimination productElimination dependent_pairFormation_alt equalityIstype promote_hyp dependent_functionElimination instantiate independent_functionElimination voidElimination isect_memberEquality_alt axiomEquality isectIsTypeImplies natural_numberEquality cumulativity intEquality imageElimination independent_pairFormation applyLambdaEquality imageMemberEquality baseClosed approximateComputation int_eqEquality Error :memTop,  dependent_set_memberEquality_alt productIsType universeEquality

Latex:
\mforall{}[I,K:Cname  List].  \mforall{}[i:\mBbbN{}2].  \mforall{}[f:name-morph(I;K)].
(((fresh-cname(I):=i)  o  f)  =  ((f)+  o  (fresh-cname(K):=i)))

Date html generated: 2020_05_21-AM-10_48_22
Last ObjectModification: 2019_12_10-PM-00_28_26

Theory : cubical!sets

Home Index