Nuprl Lemma : composition-type-lemma6

[Gamma:j⊢]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[u:{Gamma, phi.𝕀 ⊢ _:A}].
  ({Gamma ⊢ _:(A)[1(𝕀)][phi |⟶ (u)[1(𝕀)]]} ∈ 𝕌{[i j']})


Proof




Definitions occuring in Statement :  constrained-cubical-term: {Gamma ⊢ _:A[phi |⟶ t]} context-subset: Gamma, phi face-type: 𝔽 interval-1: 1(𝕀) interval-type: 𝕀 csm-id-adjoin: [u] cube-context-adjoin: X.A csm-ap-term: (t)s cubical-term: {X ⊢ _:A} csm-ap-type: (AF)s cubical-type: {X ⊢ _} cubical_set: CubicalSet uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B uimplies: supposing a csm-id-adjoin: [u] csm-id: 1(X) guard: {T}
Lemmas referenced :  constrained-cubical-term_wf csm-ap-type_wf cube-context-adjoin_wf interval-type_wf cubical_set_cumulativity-i-j csm-id-adjoin_wf-interval-1 cubical-type-cumulativity2 csm-ap-term_wf context-subset_wf subset-cubical-type sub_cubical_set_functionality context-subset-is-subset context-subset-adjoin-subtype cubical-term_wf cubical-type_wf face-type_wf cubical_set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut thin instantiate extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis applyEquality sqequalRule because_Cache independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry universeIsType isect_memberEquality_alt isectIsTypeImplies inhabitedIsType

Latex:
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].  \mforall{}[A:\{Gamma.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[u:\{Gamma,  phi.\mBbbI{}  \mvdash{}  \_:A\}].
    (\{Gamma  \mvdash{}  \_:(A)[1(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[1(\mBbbI{})]]\}  \mmember{}  \mBbbU{}\{[i  |  j']\})



Date html generated: 2020_05_20-PM-04_09_55
Last ObjectModification: 2020_04_13-PM-00_35_51

Theory : cubical!type!theory


Home Index