Nuprl Lemma : compatible-system_wf
∀[Gamma:j⊢]. ∀[sys:(phi:{Gamma ⊢ _:𝔽} × {Gamma, phi ⊢ _}) List]. (compatible-system{i:l}(Gamma;sys) ∈ ℙ{[i' | j']})
Proof
Definitions occuring in Statement :
compatible-system: compatible-system{i:l}(Gamma;sys),
context-subset: Gamma, phi,
face-type: 𝔽,
cubical-term: {X ⊢ _:A},
cubical-type: {X ⊢ _},
cubical_set: CubicalSet,
list: T List,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T,
product: x:A × B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
compatible-system: compatible-system{i:l}(Gamma;sys),
so_lambda: λ2x y.t[x; y],
subtype_rel: A ⊆r B,
uimplies: b supposing a,
so_apply: x[s1;s2]
Lemmas referenced :
pairwise_wf2,
cubical-term_wf,
face-type_wf,
cubical-type_wf,
context-subset_wf,
equal_wf,
face-and_wf,
subset-cubical-type,
face-term-implies-subset,
face-term-and-implies1,
face-term-and-implies2,
list_wf,
cubical_set_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
thin,
instantiate,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
productEquality,
cumulativity,
hypothesisEquality,
hypothesis,
lambdaEquality_alt,
spreadEquality,
applyEquality,
independent_isectElimination,
because_Cache,
inhabitedIsType,
productIsType,
universeIsType,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
isect_memberEquality_alt,
isectIsTypeImplies
Latex:
\mforall{}[Gamma:j\mvdash{}]. \mforall{}[sys:(phi:\{Gamma \mvdash{} \_:\mBbbF{}\} \mtimes{} \{Gamma, phi \mvdash{} \_\}) List].
(compatible-system\{i:l\}(Gamma;sys) \mmember{} \mBbbP{}\{[i' | j']\})
Date html generated:
2020_05_20-PM-03_09_08
Last ObjectModification:
2020_04_06-PM-11_41_59
Theory : cubical!type!theory
Home
Index