Nuprl Lemma : name-morph-extend-comp

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


Proof




Definitions occuring in Statement :  name-comp: (f g) name-morph-extend: (f)+ name-morph: name-morph(I;J) add-fresh-cname: I+ coordinate_name: Cname list: List uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B name-morph: name-morph(I;J) uimplies: supposing a name-morph-extend: (f)+ name-comp: (f g) compose: 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:  Q false: False all: x:A. B[x] bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  bfalse: ff iff: ⇐⇒ Q rev_implies:  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