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

`∀[I:Cname List]. ∀[alpha:c𝕌(I)]. ∀[L,J,K:Cname List]. ∀[f:name-morph(L;J)]. ∀[g:name-morph(J;K)]. ∀[a:name-morph(I;L)].`
`∀[T:cu-cube-family(alpha;L;a)].`
`  (cu-cube-restriction(alpha;J;K;g;(a o f);cu-cube-restriction(alpha;L;J;f;a;T))`
`  = cu-cube-restriction(alpha;L;K;(f o g);a;T)`
`  ∈ cu-cube-family(alpha;K;(a o (f o g))))`

Proof

Definitions occuring in Statement :  cu-cube-restriction: `cu-cube-restriction(alpha;L;J;f;a;T)` cu-cube-family: `cu-cube-family(alpha;L;f)` cubical-universe: `c𝕌` I-cube: `X(I)` name-comp: `(f o g)` name-morph: `name-morph(I;J)` 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` pi1: `fst(t)` cu-cube-family: `cu-cube-family(alpha;L;f)` cu-cube-restriction: `cu-cube-restriction(alpha;L;J;f;a;T)` pi2: `snd(t)` and: `P ∧ Q` squash: `↓T` prop: `ℙ` all: `∀x:A. B[x]` true: `True` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  cubical-universe-I-cube equal_wf squash_wf true_wf list_wf coordinate_name_wf name-comp_wf iff_weakening_equal cu-cube-family_wf name-morph_wf I-cube_wf cubical-universe_wf
Rules used in proof :  sqequalHypSubstitution cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesisEquality hypothesis setElimination rename productElimination sqequalRule applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality functionExtensionality because_Cache dependent_functionElimination natural_numberEquality imageMemberEquality baseClosed independent_isectElimination independent_functionElimination instantiate isect_memberFormation isect_memberEquality axiomEquality

Latex:
\mforall{}[I:Cname  List].  \mforall{}[alpha:c\mBbbU{}(I)].  \mforall{}[L,J,K:Cname  List].  \mforall{}[f:name-morph(L;J)].  \mforall{}[g:name-morph(J;K)].
\mforall{}[a:name-morph(I;L)].  \mforall{}[T:cu-cube-family(alpha;L;a)].
(cu-cube-restriction(alpha;J;K;g;(a  o  f);cu-cube-restriction(alpha;L;J;f;a;T))
=  cu-cube-restriction(alpha;L;K;(f  o  g);a;T))

Date html generated: 2017_10_05-PM-04_13_33
Last ObjectModification: 2017_07_28-AM-11_30_12

Theory : cubical!sets

Home Index