Nuprl Lemma : system-type_wf
∀[Gamma:j⊢]. ∀[sys:(phi:{Gamma ⊢ _:𝔽} × {Gamma, phi ⊢ _}) List].
Gamma, \/(map(λp.(fst(p));sys)) ⊢ system-type(sys) supposing compatible-system{i:l}(Gamma;sys)
Proof
Definitions occuring in Statement :
system-type: system-type(sys),
compatible-system: compatible-system{i:l}(Gamma;sys),
context-subset: Gamma, phi,
face-or-list: \/(L),
face-type: 𝔽,
cubical-term: {X ⊢ _:A},
cubical-type: {X ⊢ _},
cubical_set: CubicalSet,
map: map(f;as),
list: T List,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
pi1: fst(t),
member: t ∈ T,
lambda: λx.A[x],
product: x:A × B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
prop: ℙ
Lemmas referenced :
system-type-properties,
compatible-system_wf,
list_wf,
cubical-term_wf,
face-type_wf,
cubical-type_wf,
context-subset_wf,
cubical_set_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
independent_functionElimination,
hypothesis,
productElimination,
equalityTransitivity,
equalitySymmetry,
sqequalRule,
axiomEquality,
universeIsType,
isectElimination,
isect_memberEquality_alt,
isectIsTypeImplies,
inhabitedIsType,
instantiate,
productEquality,
cumulativity
Latex:
\mforall{}[Gamma:j\mvdash{}]. \mforall{}[sys:(phi:\{Gamma \mvdash{} \_:\mBbbF{}\} \mtimes{} \{Gamma, phi \mvdash{} \_\}) List].
Gamma, \mbackslash{}/(map(\mlambda{}p.(fst(p));sys)) \mvdash{} system-type(sys) supposing compatible-system\{i:l\}(Gamma;sys)
Date html generated:
2020_05_20-PM-03_09_46
Last ObjectModification:
2020_04_07-PM-00_58_33
Theory : cubical!type!theory
Home
Index