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

`∀[I,J,K:Cname List]. ∀[f:name-morph(I;J)]. ∀[g:name-morph(J;K)].  (((f o g))+ = ((f)+ o (g)+) ∈ name-morph(I+;K+))`

Proof

Definitions occuring in Statement :  name-comp: `(f o g)` name-morph-extend: `(f)+` name-morph: `name-morph(I;J)` add-fresh-cname: `I+` coordinate_name: `Cname` list: `T List` uall: `∀[x:A]. B[x]` 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)` compose: `f o g` has-value: `(a)↓` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` eq-cname: `eq-cname(x;y)` uext: `uext(g)` nameset: `nameset(L)` not: `¬A` implies: `P `` Q` false: `False` all: `∀x:A. B[x]` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` ifthenelse: `if b then t else f fi ` bfalse: `ff` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` coordinate_name: `Cname` int_upper: `{i...}` isname: `isname(z)` true: `True` assert: `↑b` sq_type: `SQType(T)` guard: `{T}` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` add-fresh-cname: `I+` or: `P ∨ Q`
Lemmas referenced :  name-morphs-equal add-fresh-cname_wf name-morph-extend_wf name-comp_wf name-morph_wf list_wf coordinate_name_wf value-type-has-value not_wf l_member_wf set-value-type coordinate_name-value-type fresh-cname_wf nameset_wf eq-cname_wf bool_wf equal-wf-T-base assert_wf equal_wf bnot_wf assert_elim btrue_neq_bfalse uiff_transitivity eqtt_to_assert assert-eq-cname iff_transitivity iff_weakening_uiff eqff_to_assert assert_of_bnot set_wf subtype_base_sq bool_subtype_base iff_imp_equal_bool le_int_wf btrue_wf le_wf true_wf assert_of_le_int iff_wf satisfiable-full-omega-tt intformnot_wf intformeq_wf itermVar_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_wf cons_member nameset_subtype_extd-nameset isname_wf assert-isname set_subtype_base int_subtype_base fresh-cname-not-member extd-nameset_subtype l_subset_right_cons_trivial not-assert-isname nsub2_subtype_extd-nameset
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality lambdaEquality setElimination rename sqequalRule independent_isectElimination isect_memberEquality axiomEquality because_Cache callbyvalueReduce setEquality baseClosed equalityTransitivity equalitySymmetry addLevel levelHypothesis independent_functionElimination voidElimination lambdaFormation unionElimination equalityElimination productElimination independent_pairFormation impliesFunctionality dependent_functionElimination instantiate cumulativity natural_numberEquality dependent_pairFormation int_eqEquality intEquality voidEquality computeAll dependent_set_memberEquality inlFormation

Latex:
\mforall{}[I,J,K:Cname  List].  \mforall{}[f:name-morph(I;J)].  \mforall{}[g:name-morph(J;K)].    (((f  o  g))+  =  ((f)+  o  (g)+))

Date html generated: 2017_10_05-AM-10_07_08
Last ObjectModification: 2017_07_28-AM-11_16_32

Theory : cubical!sets

Home Index