Nuprl Lemma : compU_wf1
∀[G:j⊢]. (compU() ∈ composition-function{j:l, i':l}(G; c𝕌))
Proof
Definitions occuring in Statement :
compU: compU(),
cubical-universe: c𝕌,
composition-function: composition-function{j:l,i:l}(Gamma;A),
cubical_set: CubicalSet,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
compU: compU(),
composition-function: composition-function{j:l,i:l}(Gamma;A)
Lemmas referenced :
csm-cubical-universe,
compU-wf-lemma1,
istype-cubical-term,
face-type_wf,
cube_set_map_wf,
cube-context-adjoin_wf,
interval-type_wf,
cubical_set_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
lambdaEquality_alt,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
Error :memTop,
hypothesis,
because_Cache,
rename,
hypothesisEquality,
universeIsType,
instantiate,
inhabitedIsType,
axiomEquality,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[G:j\mvdash{}]. (compU() \mmember{} composition-function\{j:l, i':l\}(G; c\mBbbU{}))
Date html generated:
2020_05_20-PM-07_22_38
Last ObjectModification:
2020_04_27-PM-05_59_28
Theory : cubical!type!theory
Home
Index