Nuprl Lemma : cu-cube-family-comp
∀[I:Cname List]. ∀[alpha:c𝕌(I)]. ∀[J,L,f,g:Top]. (cu-cube-family(alpha;L;(f o g)) ~ cu-cube-family(f(alpha);L;g))
Proof
Definitions occuring in Statement :
cu-cube-family: cu-cube-family(alpha;L;f),
cubical-universe: c𝕌,
cube-set-restriction: f(s),
I-cube: X(I),
name-comp: (f o g),
coordinate_name: Cname,
list: T List,
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
pi1: fst(t),
cubical-universe: c𝕌,
cube-set-restriction: f(s),
cu-cube-family: cu-cube-family(alpha;L;f),
pi2: snd(t),
unit-cube-map: unit-cube-map(f),
csm-Kan-cubical-type: (AK)s,
csm-ap-type: (AF)s,
csm-ap: (s)x
Lemmas referenced :
cubical-universe-I-cube,
top_wf,
I-cube_wf,
cubical-universe_wf,
list_wf,
coordinate_name_wf
Rules used in proof :
sqequalHypSubstitution,
cut,
lemma_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
setElimination,
rename,
productElimination,
sqequalRule,
because_Cache,
instantiate,
isect_memberFormation,
introduction,
sqequalAxiom,
isect_memberEquality
Latex:
\mforall{}[I:Cname List]. \mforall{}[alpha:c\mBbbU{}(I)]. \mforall{}[J,L,f,g:Top].
(cu-cube-family(alpha;L;(f o g)) \msim{} cu-cube-family(f(alpha);L;g))
Date html generated:
2016_06_16-PM-08_07_19
Last ObjectModification:
2015_12_28-PM-04_11_37
Theory : cubical!sets
Home
Index