Nuprl Lemma : cube-set-restriction-comp2

X:CubicalSet. ∀I,J,J2,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I).
  g(f(a)) (f g)(a) ∈ X(K) supposing J2 ∈ (Cname List)


Proof




Definitions occuring in Statement :  cube-set-restriction: f(s) I-cube: X(I) cubical-set: CubicalSet name-comp: (f g) name-morph: name-morph(I;J) coordinate_name: Cname list: List uimplies: supposing a all: x:A. B[x] equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uimplies: supposing a and: P ∧ Q member: t ∈ T uall: [x:A]. B[x] prop: subtype_rel: A ⊆B coordinate_name: Cname int_upper: {i...} so_lambda: λ2x.t[x] so_apply: x[s] sq_type: SQType(T) implies:  Q guard: {T} rev_implies:  Q squash: T true: True iff: ⇐⇒ Q
Lemmas referenced :  and_wf equal_wf list_wf coordinate_name_wf cube-set-restriction_wf subtype_base_sq list_subtype_base set_subtype_base le_wf int_subtype_base subtype_rel_self name-morph_wf I-cube_wf squash_wf true_wf length_wf_nat nat_wf subtype_rel_wf member_wf cube-set-restriction-comp iff_weakening_equal all_wf cubical-set_wf isect_wf
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation dependent_set_memberEquality hypothesis independent_pairFormation hypothesisEquality introduction extract_by_obid sqequalHypSubstitution isectElimination thin applyLambdaEquality setElimination rename productElimination applyEquality instantiate cumulativity independent_isectElimination sqequalRule intEquality lambdaEquality natural_numberEquality dependent_functionElimination independent_functionElimination equalitySymmetry because_Cache addLevel allFunctionality imageElimination equalityTransitivity universeEquality hyp_replacement imageMemberEquality baseClosed

Latex:
\mforall{}X:CubicalSet.  \mforall{}I,J,J2,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).  \mforall{}a:X(I).
    g(f(a))  =  (f  o  g)(a)  supposing  J  =  J2



Date html generated: 2017_10_05-AM-10_12_01
Last ObjectModification: 2017_03_03-AM-01_52_42

Theory : cubical!sets


Home Index