Nuprl Lemma : univ-comp-sq
∀[G:Top]. (univ-comp{i:l}() ~ cfun-to-cop(G;c𝕌;compU()))
Proof
Definitions occuring in Statement :
univ-comp: univ-comp{i:l}(),
compU: compU(),
cubical-universe: c𝕌,
comp-fun-to-comp-op: cfun-to-cop(Gamma;A;comp),
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
comp-fun-to-comp-op: cfun-to-cop(Gamma;A;comp),
univ-comp: univ-comp{i:l}(),
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>,
cubical-universe: c𝕌,
compU: compU(),
closed-cubical-universe: cc𝕌,
closed-type-to-type: closed-type-to-type(T),
all: ∀x:A. B[x],
member: t ∈ T
Lemmas referenced :
cubical_type_ap_morph_pair_lemma,
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
sqequalRule,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
Error :memTop,
hypothesis
Latex:
\mforall{}[G:Top]. (univ-comp\{i:l\}() \msim{} cfun-to-cop(G;c\mBbbU{};compU()))
Date html generated:
2020_05_20-PM-07_23_32
Last ObjectModification:
2020_04_25-PM-10_00_18
Theory : cubical!type!theory
Home
Index