Nuprl Lemma : csm-cubical-universe
∀[s:Top]. ((c𝕌)s ~ c𝕌)
Proof
Definitions occuring in Statement :
cubical-universe: c𝕌,
csm-ap-type: (AF)s,
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Definitions unfolded in proof :
cubical-universe: c𝕌,
uall: ∀[x:A]. B[x],
member: t ∈ T
Lemmas referenced :
csm-closed-type,
closed-cubical-universe_wf,
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
thin,
instantiate,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
hypothesis,
hypothesisEquality,
axiomSqEquality
Latex:
\mforall{}[s:Top]. ((c\mBbbU{})s \msim{} c\mBbbU{})
Date html generated:
2020_05_20-PM-07_08_29
Last ObjectModification:
2020_04_25-PM-01_33_06
Theory : cubical!type!theory
Home
Index