Nuprl Lemma : ctt-term-type-is_wf
∀[X:⊢''']. ∀[t:cttTerm(X)]. ∀[T:{X ⊢''' _}]. (type(t)=T ∈ ℙ{i''''})
Proof
Definitions occuring in Statement :
ctt-term-type-is: type(t)=T,
ctt-term-meaning: cttTerm(X),
cubical-type: {X ⊢ _},
cubical_set: CubicalSet,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
ctt-term-type-is: type(t)=T,
member: t ∈ T,
subtype_rel: A ⊆r B
Lemmas referenced :
ctt-term-type_wf,
ctt-level-type-subtype,
ctt-term-level_wf,
equal_wf,
cubical-type_wf,
ctt-term-meaning_wf,
cubical_set_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
applyEquality,
sqequalRule,
instantiate,
universeIsType
Latex:
\mforall{}[X:\mvdash{}''']. \mforall{}[t:cttTerm(X)]. \mforall{}[T:\{X \mvdash{}''' \_\}]. (type(t)=T \mmember{} \mBbbP{}\{i''''\})
Date html generated:
2020_05_20-PM-07_52_07
Last ObjectModification:
2020_05_05-PM-02_05_51
Theory : cubical!type!theory
Home
Index