### Nuprl Lemma : face-map-comp

`∀A,B:Cname List. ∀g:name-morph(A;B). ∀x:nameset(A). ∀i:ℕ2.`
`  (g o (g x:=i)) = ((x:=i) o g) ∈ name-morph(A;B-[g x]) supposing ↑isname(g x)`

Proof

Definitions occuring in Statement :  name-comp: `(f o g)` face-map: `(x:=i)` name-morph: `name-morph(I;J)` isname: `isname(z)` nameset: `nameset(L)` cname_deq: `CnameDeq` coordinate_name: `Cname` list-diff: `as-bs` cons: `[a / b]` nil: `[]` list: `T List` int_seg: `{i..j-}` assert: `↑b` uimplies: `b supposing a` all: `∀x:A. B[x]` apply: `f a` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` member: `t ∈ T` name-morph: `name-morph(I;J)` uiff: `uiff(P;Q)` and: `P ∧ Q` subtype_rel: `A ⊆r B` guard: `{T}` nameset: `nameset(L)` face-map: `(x:=i)` name-comp: `(f o g)` uext: `uext(g)` compose: `f o g` coordinate_name: `Cname` int_upper: `{i...}` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` bnot: `¬bb` assert: `↑b` false: `False` isname: `isname(z)` int_seg: `{i..j-}` prop: `ℙ` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` lelt: `i ≤ j < k` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` true: `True` decidable: `Dec(P)` squash: `↓T` cand: `A c∧ B` nequal: `a ≠ b ∈ T ` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  assert-isname istype-assert isname_wf int_seg_wf nameset_wf name-morph_wf name-morphs-equal list-diff_wf coordinate_name_wf cname_deq_wf cons_wf nil_wf name-comp_wf face-map_wf2 eq_int_wf eqtt_to_assert assert_of_eq_int eqff_to_assert bool_subtype_base bool_cases_sqequal subtype_base_sq bool_wf assert-bnot neg_assert_of_eq_int iff_imp_equal_bool le_int_wf bfalse_wf iff_functionality_wrt_iff assert_wf le_wf false_wf iff_weakening_uiff assert_of_le_int iff_weakening_equal int_seg_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma istype-void 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 nsub2_subtype_extd-nameset btrue_wf true_wf decidable__assert not-assert-isname member-list-diff member_singleton l_member_wf nameset_subtype_extd-nameset nameset_subtype_base decidable__equal_int intformnot_wf intformeq_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma set_subtype_base int_subtype_base equal_wf squash_wf istype-universe eq_int_eq_true extd-nameset_subtype_int subtype_rel_self
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt isect_memberFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality setElimination rename because_Cache hypothesis productElimination independent_isectElimination universeIsType natural_numberEquality equalityTransitivity equalitySymmetry lambdaEquality_alt inhabitedIsType sqequalRule unionElimination equalityElimination dependent_pairFormation_alt equalityIsType3 promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination voidElimination equalityIsType1 independent_pairFormation approximateComputation int_eqEquality isect_memberEquality_alt applyLambdaEquality imageMemberEquality baseClosed imageElimination dependent_set_memberEquality_alt intEquality closedConclusion universeEquality

Latex:
\mforall{}A,B:Cname  List.  \mforall{}g:name-morph(A;B).  \mforall{}x:nameset(A).  \mforall{}i:\mBbbN{}2.
(g  o  (g  x:=i))  =  ((x:=i)  o  g)  supposing  \muparrow{}isname(g  x)

Date html generated: 2019_11_05-PM-00_24_42
Last ObjectModification: 2018_11_08-PM-00_27_32

Theory : cubical!sets

Home Index