Nuprl Lemma : cubical-set_wf
CubicalSet ∈ 𝕌'
Proof
Definitions occuring in Statement :
cubical-set: CubicalSet,
member: t ∈ T,
universe: Type
Definitions unfolded in proof :
cubical-set: CubicalSet,
member: t ∈ T,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
and: P ∧ Q,
so_lambda: λ2x.t[x],
so_apply: x[s],
prop: ℙ
Lemmas referenced :
list_wf,
coordinate_name_wf,
subtype_rel_universe1,
name-morph_wf,
all_wf,
equal_wf,
name-comp_wf,
compose_wf,
equal-wf-T-base,
id-morph_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
setEquality,
productEquality,
closedConclusion,
functionEquality,
cumulativity,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesis,
universeEquality,
applyEquality,
because_Cache,
hypothesisEquality,
productElimination,
lambdaEquality_alt,
universeIsType,
inhabitedIsType,
equalityTransitivity,
equalitySymmetry,
baseClosed
Latex:
CubicalSet \mmember{} \mBbbU{}'
Date html generated:
2019_11_05-PM-00_25_24
Last ObjectModification:
2018_12_10-AM-09_36_30
Theory : cubical!sets
Home
Index