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