Nuprl Lemma : cubical-path-1_wf

[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[I:fset(ℕ)]. ∀[i:{i:ℕ| ¬i ∈ I} ]. ∀[rho:Gamma(I+i)]. ∀[phi:𝔽(I)].
[u:{I+i,s(phi) ⊢ _:(A)<rho> iota}].
  (cubical-path-1(Gamma;A;I;i;rho;phi;u) ∈ 𝕌{[i' j']})


Proof




Definitions occuring in Statement :  cubical-path-1: cubical-path-1(Gamma;A;I;i;rho;phi;u) cubical-term: {X ⊢ _:A} csm-ap-type: (AF)s cubical-type: {X ⊢ _} subset-iota: iota cubical-subset: I,psi face-presheaf: 𝔽 csm-comp: F context-map: <rho> formal-cube: formal-cube(I) cube-set-restriction: f(s) I_cube: A(I) cubical_set: CubicalSet nc-s: s add-name: I+i fset-member: a ∈ s fset: fset(T) int-deq: IntDeq nat: uall: [x:A]. B[x] not: ¬A member: t ∈ T set: {x:A| B[x]}  universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T cubical-path-1: cubical-path-1(Gamma;A;I;i;rho;phi;u) subtype_rel: A ⊆B not: ¬A implies:  Q prop: false: False uimplies: supposing a all: x:A. B[x] nat: ge: i ≥  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] and: P ∧ Q so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  cubical-type-at_wf cube-set-restriction_wf add-name_wf nc-1_wf cubical-path-condition'_wf cubical-type-cumulativity2 cubical_set_cumulativity-i-j fset-member_wf nat_wf int-deq_wf istype-void cubical-term_wf cubical-subset_wf face-presheaf_wf2 nc-s_wf f-subset-add-name csm-ap-type_wf cubical-type-cumulativity csm-comp_wf formal-cube_wf1 subset-iota_wf context-map_wf I_cube_wf nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf istype-le istype-nat strong-subtype-deq-subtype strong-subtype-set3 le_wf strong-subtype-self fset_wf cubical-type_wf cubical_set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut setElimination thin rename sqequalRule setEquality cumulativity extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis instantiate applyEquality because_Cache dependent_set_memberEquality_alt functionIsType universeIsType axiomEquality equalityTransitivity equalitySymmetry independent_isectElimination dependent_functionElimination isect_memberEquality_alt isectIsTypeImplies inhabitedIsType natural_numberEquality unionElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality Error :memTop,  independent_pairFormation voidElimination setIsType intEquality

Latex:
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  ].  \mforall{}[rho:Gamma(I+i)].  \mforall{}[phi:\mBbbF{}(I)].
\mforall{}[u:\{I+i,s(phi)  \mvdash{}  \_:(A)<rho>  o  iota\}].
    (cubical-path-1(Gamma;A;I;i;rho;phi;u)  \mmember{}  \mBbbU{}\{[i'  |  j']\})



Date html generated: 2020_05_20-PM-03_46_35
Last ObjectModification: 2020_04_09-AM-11_08_32

Theory : cubical!type!theory


Home Index