Nuprl Lemma : csm-cubical-path-1-subtype

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


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 csm-ap: (s)x context-map: <rho> cube_set_map: A ⟶ B 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: subtype_rel: A ⊆B uall: [x:A]. B[x] not: ¬A set: {x:A| B[x]} 
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B uimplies: supposing a all: x:A. B[x] nat: ge: i ≥  decidable: Dec(P) or: P ∨ Q not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False and: P ∧ Q prop: so_lambda: λ2x.t[x] so_apply: x[s] squash: T true: True cube_set_map: A ⟶ B psc_map: A ⟶ B nat-trans: nat-trans(C;D;F;G) cat-ob: cat-ob(C) pi1: fst(t) op-cat: op-cat(C) spreadn: spread4 cube-cat: CubeCat fset: fset(T) quotient: x,y:A//B[x; y] cat-arrow: cat-arrow(C) pi2: snd(t) type-cat: TypeCat names-hom: I ⟶ J cat-comp: cat-comp(C) compose: g guard: {T} iff: ⇐⇒ Q rev_implies:  Q cubical-path-1: cubical-path-1(Gamma;A;I;i;rho;phi;u) cubical-path-condition': cubical-path-condition'(Gamma;A;I;i;rho;phi;u;a1)
Lemmas referenced :  cubical-term_wf cubical-subset_wf add-name_wf cube-set-restriction_wf face-presheaf_wf2 nc-s_wf f-subset-add-name csm-ap-type_wf cubical_set_cumulativity-i-j 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 fset-member_wf nat_wf int-deq_wf strong-subtype-deq-subtype strong-subtype-set3 le_wf strong-subtype-self istype-void fset_wf cubical-type_wf cube_set_map_wf cubical_set_wf squash_wf true_wf cubical-type-cumulativity2 csm-ap_wf equal_wf csm-ap-comp-type subtype_rel_self iff_weakening_equal csm-comp-context-map istype-universe cubical-path-1_wf subtype_rel-equal cubical-type-at_wf nc-1_wf csm-ap-type-at csm-ap-restriction cubical-subset-I_cube-member csm-cubical-type-ap-morph cubical-type-ap-morph_wf trivial-equal names-hom_wf istype-cubical-type-at cubical-path-condition'_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule axiomEquality hypothesis universeIsType thin instantiate extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality setElimination rename because_Cache independent_isectElimination dependent_functionElimination applyEquality isect_memberEquality_alt isectIsTypeImplies inhabitedIsType dependent_set_memberEquality_alt natural_numberEquality unionElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality Error :memTop,  independent_pairFormation voidElimination setIsType functionIsType intEquality imageElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed productElimination universeEquality hyp_replacement promote_hyp lambdaFormation_alt

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



Date html generated: 2020_05_20-PM-03_48_16
Last ObjectModification: 2020_04_09-PM-01_09_29

Theory : cubical!type!theory


Home Index