### Nuprl Lemma : cube-set-restriction-comp

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

Proof

Definitions occuring in Statement :  cube-set-restriction: `f(s)` I-cube: `X(I)` cubical-set: `CubicalSet` name-comp: `(f o g)` name-morph: `name-morph(I;J)` coordinate_name: `Cname` list: `T List` all: `∀x:A. B[x]` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` cubical-set: `CubicalSet` cube-set-restriction: `f(s)` pi2: `snd(t)` and: `P ∧ Q` squash: `↓T` uall: `∀[x:A]. B[x]` prop: `ℙ` I-cube: `X(I)` top: `Top` subtype_rel: `A ⊆r B` functor-ob: `ob(F)` pi1: `fst(t)` true: `True` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` compose: `f o g`
Lemmas referenced :  equal_wf squash_wf true_wf I-cube_wf list_wf coordinate_name_wf ob_pair_lemma subtype_rel_self iff_weakening_equal compose_wf name-morph_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesisEquality sqequalHypSubstitution setElimination thin rename productElimination sqequalRule applyEquality lambdaEquality imageElimination introduction extract_by_obid isectElimination equalityTransitivity hypothesis equalitySymmetry universeEquality functionExtensionality because_Cache dependent_functionElimination isect_memberEquality voidElimination voidEquality natural_numberEquality imageMemberEquality baseClosed independent_isectElimination independent_functionElimination

Latex:
\mforall{}X:CubicalSet.  \mforall{}I,J,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))

Date html generated: 2017_10_05-AM-10_11_58
Last ObjectModification: 2017_07_28-AM-11_18_01

Theory : cubical!sets

Home Index