### Nuprl Lemma : extend-name-morph-iota

`∀I,K:Cname List. ∀f:name-morph(I;K). ∀z,x:Cname.`
`  (iota(z) o f[z:=x]) = (f o iota(x)) ∈ name-morph(I;[x / K]) supposing (¬(x ∈ K)) ∧ (¬(z ∈ I))`

Proof

Definitions occuring in Statement :  name-comp: `(f o g)` iota: `iota(x)` extend-name-morph: `f[z1:=z2]` name-morph: `name-morph(I;J)` coordinate_name: `Cname` l_member: `(x ∈ l)` cons: `[a / b]` list: `T List` uimplies: `b supposing a` all: `∀x:A. B[x]` not: `¬A` and: `P ∧ Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uimplies: `b supposing a` and: `P ∧ Q` uall: `∀[x:A]. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` name-morph: `name-morph(I;J)` prop: `ℙ` iota: `iota(x)` name-comp: `(f o g)` extend-name-morph: `f[z1:=z2]` compose: `f o g` uext: `uext(g)` ifthenelse: `if b then t else f fi ` btrue: `tt` nameset: `nameset(L)` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` uiff: `uiff(P;Q)` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` coordinate_name: `Cname` int_upper: `{i...}` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  name-morphs-equal cons_wf coordinate_name_wf name-comp_wf iota_wf extend-name-morph_wf name-morph_wf not_wf l_member_wf nameset_wf isname-nameset eq-cname_wf bool_wf eqtt_to_assert assert-eq-cname eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot set_subtype_base le_wf int_subtype_base isname_wf extd-nameset_subtype l_subset_right_cons_trivial
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut sqequalHypSubstitution productElimination thin introduction extract_by_obid isectElimination hypothesisEquality hypothesis independent_isectElimination because_Cache applyEquality lambdaEquality setElimination rename sqequalRule productEquality functionExtensionality unionElimination equalityElimination equalityTransitivity equalitySymmetry dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination voidElimination intEquality natural_numberEquality

Latex:
\mforall{}I,K:Cname  List.  \mforall{}f:name-morph(I;K).  \mforall{}z,x:Cname.
(iota(z)  o  f[z:=x])  =  (f  o  iota(x))  supposing  (\mneg{}(x  \mmember{}  K))  \mwedge{}  (\mneg{}(z  \mmember{}  I))

Date html generated: 2017_10_05-AM-10_08_34
Last ObjectModification: 2017_07_28-AM-11_16_55

Theory : cubical!sets

Home Index