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

`∀[I:Cname List]. ∀[alpha:c𝕌(I)]. ∀[K:Cname List]. ∀[a:name-morph(I;K)]. ∀[T:cu-cube-family(alpha;K;a)].`
`  (cu-cube-restriction(alpha;K;K;1;a;T) = T ∈ cu-cube-family(alpha;K;a))`

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)` id-morph: `1` 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 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 dependent_functionElimination because_Cache 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{}[K:Cname  List].  \mforall{}[a:name-morph(I;K)].
\mforall{}[T:cu-cube-family(alpha;K;a)].
(cu-cube-restriction(alpha;K;K;1;a;T)  =  T)

Date html generated: 2017_10_05-PM-04_13_27
Last ObjectModification: 2017_07_28-AM-11_30_05

Theory : cubical!sets

Home Index