Nuprl Lemma : term-context-subset-subtype
∀[Gamma:j⊢]. ∀[phi1,phi2:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma ⊢ _}].
{Gamma, phi1 ⊢ _:A} ⊆r {Gamma, phi2 ⊢ _:A} supposing Gamma ⊢ (phi2 ⇒ phi1)
Proof
Definitions occuring in Statement :
face-term-implies: Gamma ⊢ (phi ⇒ psi),
context-subset: Gamma, phi,
face-type: 𝔽,
cubical-term: {X ⊢ _:A},
cubical-type: {X ⊢ _},
cubical_set: CubicalSet,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
member: t ∈ T,
prop: ℙ
Lemmas referenced :
subset-cubical-term,
context-subset_wf,
face-term-implies-subset,
thin-context-subset,
face-term-implies_wf,
cubical-type_wf,
cubical-term_wf,
face-type_wf,
cubical_set_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
independent_isectElimination,
universeIsType,
instantiate,
because_Cache
Latex:
\mforall{}[Gamma:j\mvdash{}]. \mforall{}[phi1,phi2:\{Gamma \mvdash{} \_:\mBbbF{}\}]. \mforall{}[A:\{Gamma \mvdash{} \_\}].
\{Gamma, phi1 \mvdash{} \_:A\} \msubseteq{}r \{Gamma, phi2 \mvdash{} \_:A\} supposing Gamma \mvdash{} (phi2 {}\mRightarrow{} phi1)
Date html generated:
2020_05_20-PM-02_55_12
Last ObjectModification:
2020_04_06-AM-10_31_35
Theory : cubical!type!theory
Home
Index