### Nuprl Lemma : cubical-term_wf

`∀[X:j⊢]. ∀[A:{X ⊢ _}].  ({X ⊢ _:A} ∈ 𝕌{[i | j']})`

Proof

Definitions occuring in Statement :  cubical-term: `{X ⊢ _:A}` cubical-type: `{X ⊢ _}` cubical_set: `CubicalSet` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` cubical-type: `{X ⊢ _}` cubical-term: `{X ⊢ _:A}` all: `∀x:A. B[x]` prop: `ℙ`
Lemmas referenced :  cubical_type_at_pair_lemma cubical_type_ap_morph_pair_lemma fset_wf nat_wf I_cube_wf names-hom_wf equal_wf cube-set-restriction_wf cubical-type_wf cubical_set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut sqequalHypSubstitution setElimination thin rename productElimination sqequalRule introduction extract_by_obid dependent_functionElimination Error :memTop,  hypothesis setEquality functionEquality cumulativity isectElimination hypothesisEquality applyEquality universeIsType instantiate

Latex:
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].    (\{X  \mvdash{}  \_:A\}  \mmember{}  \mBbbU{}\{[i  |  j']\})

Date html generated: 2020_05_20-PM-01_51_13
Last ObjectModification: 2020_04_07-PM-00_18_05

Theory : cubical!type!theory

Home Index