Nuprl Lemma : composition-op-1-case1

[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[cA:Gamma ⊢ CompOp(A)]. ∀[I:fset(ℕ)]. ∀[i:{i:ℕ| ¬i ∈ I} ]. ∀[rho:Gamma(I+i)].
[u:{I+i,s(1) ⊢ _:(A)<rho> iota}]. ∀[a:cubical-path-0(Gamma;A;I;i;rho;1;u)].
  ((cA rho a) u((i1)) ∈ A((i1)(rho)))


Proof




Definitions occuring in Statement :  composition-op: Gamma ⊢ CompOp(A) cubical-path-0: cubical-path-0(Gamma;A;I;i;rho;phi;u) cubical-term-at: u(a) cubical-term: {X ⊢ _:A} csm-ap-type: (AF)s cubical-type-at: A(a) cubical-type: {X ⊢ _} subset-iota: iota cubical-subset: I,psi face-presheaf: 𝔽 face_lattice: face_lattice(I) csm-comp: F context-map: <rho> formal-cube: formal-cube(I) cube-set-restriction: f(s) I_cube: A(I) cubical_set: CubicalSet nc-1: (i1) 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 set: {x:A| B[x]}  apply: a equal: t ∈ T lattice-1: 1
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B lattice-point: Point(l) record-select: r.x face_lattice: face_lattice(I) face-lattice: face-lattice(T;eq) free-dist-lattice-with-constraints: free-dist-lattice-with-constraints(T;eq;x.Cs[x]) constrained-antichain-lattice: constrained-antichain-lattice(T;eq;P) mk-bounded-distributive-lattice: mk-bounded-distributive-lattice mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o) record-update: r[x := v] ifthenelse: if then else fi  eq_atom: =a y bfalse: ff btrue: tt I_cube: A(I) functor-ob: ob(F) pi1: fst(t) face-presheaf: 𝔽 uimplies: supposing a all: x:A. B[x] bdd-distributive-lattice: BoundedDistributiveLattice 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 composition-op: Gamma ⊢ CompOp(A) cubical-path-1: cubical-path-1(Gamma;A;I;i;rho;phi;u) guard: {T} iff: ⇐⇒ Q rev_implies:  Q context-map: <rho> subset-iota: iota csm-comp: F csm-ap: (s)x compose: g functor-arrow: arrow(F) cube-set-restriction: f(s)
Lemmas referenced :  composition-op-1 nh-id_wf cubical-path-0_wf cubical-type-cumulativity2 cubical_set_cumulativity-i-j lattice-1_wf face_lattice_wf subtype_rel_self I_cube_wf face-presheaf_wf2 cubical-term_wf cubical-subset_wf add-name_wf cube-set-restriction_wf 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 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 composition-op_wf cubical-type_wf cubical_set_wf equal_wf squash_wf true_wf istype-universe subtype_rel-equal cubical-type-at_wf nc-1_wf cube-set-restriction-id subtype_rel_set cubical-path-condition'_wf istype-cubical-type-at cubical-type-ap-morph-id iff_weakening_equal csm-ap-type-at cubical-term-at_wf cubical-subset-I_cube name-morph-satisfies_wf face-presheaf-restriction-1 name-morph-1-satisfies nh-id-left
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality universeIsType instantiate applyEquality because_Cache sqequalRule setElimination rename independent_isectElimination dependent_functionElimination lambdaEquality_alt inhabitedIsType equalityTransitivity equalitySymmetry dependent_set_memberEquality_alt natural_numberEquality unionElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality Error :memTop,  independent_pairFormation voidElimination setIsType functionIsType intEquality hyp_replacement imageElimination universeEquality imageMemberEquality baseClosed cumulativity productElimination

Latex:
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[cA:Gamma  \mvdash{}  CompOp(A)].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  ].
\mforall{}[rho:Gamma(I+i)].  \mforall{}[u:\{I+i,s(1)  \mvdash{}  \_:(A)<rho>  o  iota\}].  \mforall{}[a:cubical-path-0(Gamma;A;I;i;rho;1;u)].
    ((cA  I  i  rho  1  u  a)  =  u((i1)))



Date html generated: 2020_05_20-PM-03_52_34
Last ObjectModification: 2020_04_09-PM-01_48_43

Theory : cubical!type!theory


Home Index