Nuprl Lemma : csm-univ-comp
∀[s:Top]. ((univ-comp{i:l}())s ~ univ-comp{i:l}())
Proof
Definitions occuring in Statement :
univ-comp: univ-comp{i:l}(),
csm-composition: (comp)sigma,
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Definitions unfolded in proof :
univ-comp: univ-comp{i:l}(),
comp-fun-to-comp-op: cfun-to-cop(Gamma;A;comp),
comp-fun-to-comp-op1: comp-fun-to-comp-op1(Gamma;A;comp),
canonical-section: canonical-section(Gamma;A;I;rho;a),
context-map: <rho>,
csm-composition: (comp)sigma,
cubical-universe: c𝕌,
compU: compU(),
uall: ∀[x:A]. B[x],
member: t ∈ T,
cube-set-restriction: f(s),
pi2: snd(t),
trivial-cube-set: (),
it: ⋅,
nil: []
Lemmas referenced :
void-list-equality,
nil_wf,
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
sqequalRule,
isect_memberFormation_alt,
introduction,
cut,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis,
voidEquality,
because_Cache,
axiomSqEquality
Latex:
\mforall{}[s:Top]. ((univ-comp\{i:l\}())s \msim{} univ-comp\{i:l\}())
Date html generated:
2020_05_20-PM-07_24_19
Last ObjectModification:
2020_04_25-PM-10_03_44
Theory : cubical!type!theory
Home
Index