Nuprl Lemma : cubical-term-at_wf1

[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[I:fset(ℕ)]. ∀[a:X(I)].  (u(a) ∈ A(a))


Proof




Definitions occuring in Statement :  cubical-term-at: u(a) cubical-term: {X ⊢ _:A} cubical-type-at: A(a) cubical-type: {X ⊢ _} I_cube: A(I) cubical_set: CubicalSet fset: fset(T) nat: uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T cubical-term: {X ⊢ _:A} cubical-term-at: u(a) subtype_rel: A ⊆B
Lemmas referenced :  I_cube_wf fset_wf nat_wf cubical-term_wf cubical_set_cumulativity-i-j cubical-type-cumulativity-i-j cubical-type_wf cubical_set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution setElimination thin rename sqequalRule applyEquality hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry universeIsType instantiate extract_by_obid isectElimination isect_memberEquality_alt isectIsTypeImplies inhabitedIsType

Latex:
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[u:\{X  \mvdash{}  \_:A\}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[a:X(I)].    (u(a)  \mmember{}  A(a))



Date html generated: 2020_05_20-PM-01_51_46
Last ObjectModification: 2020_03_28-PM-00_34_25

Theory : cubical!type!theory


Home Index