Nuprl Lemma : closed-term-to-term_wf
∀[T:{ * ⊢ _}]. ∀[t:closed-cubical-term(T)]. ∀[X:j⊢]. (closed-term-to-term(t) ∈ {X ⊢ _:closed-type-to-type(T)})
Proof
Definitions occuring in Statement :
closed-term-to-term: closed-term-to-term(t),
closed-cubical-term: closed-cubical-term(T),
cubical-term: {X ⊢ _:A},
closed-type-to-type: closed-type-to-type(T),
closed-cubical-type: { * ⊢ _},
cubical_set: CubicalSet,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
closed-term-to-term: closed-term-to-term(t),
closed-cubical-type: { * ⊢ _},
closed-cubical-term: closed-cubical-term(T),
pi1: fst(t),
pi2: snd(t),
closed-type-to-type: closed-type-to-type(T),
cubical-term: {X ⊢ _:A},
all: ∀x:A. B[x],
and: P ∧ Q,
subtype_rel: A ⊆r B,
cubical-type-at: A(a),
guard: {T}
Lemmas referenced :
cubical_type_at_pair_lemma,
I_cube_wf,
fset_wf,
nat_wf,
cubical_type_ap_morph_pair_lemma,
names-hom_wf,
subtype_rel_self,
cube-set-restriction_wf,
cubical_set_wf,
closed-cubical-term_wf,
closed-cubical-type_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
sqequalHypSubstitution,
setElimination,
thin,
rename,
productElimination,
dependent_set_memberEquality_alt,
extract_by_obid,
dependent_functionElimination,
Error :memTop,
hypothesis,
lambdaEquality_alt,
applyEquality,
hypothesisEquality,
universeIsType,
instantiate,
isectElimination,
lambdaFormation_alt,
inhabitedIsType,
functionIsType,
because_Cache,
equalityIstype,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
isect_memberEquality_alt,
isectIsTypeImplies
Latex:
\mforall{}[T:\{ * \mvdash{} \_\}]. \mforall{}[t:closed-cubical-term(T)]. \mforall{}[X:j\mvdash{}].
(closed-term-to-term(t) \mmember{} \{X \mvdash{} \_:closed-type-to-type(T)\})
Date html generated:
2020_05_20-PM-01_53_07
Last ObjectModification:
2020_03_20-PM-00_35_28
Theory : cubical!type!theory
Home
Index