Nuprl Lemma : face-forall-q=0

[Gamma:j⊢]. ((Gamma ⊢ ∀ (q=0)) 0(𝔽) ∈ {Gamma ⊢ _:𝔽})


Proof




Definitions occuring in Statement :  face-forall: (∀ phi) face-zero: (i=0) face-0: 0(𝔽) face-type: 𝔽 cc-snd: q cubical-term: {X ⊢ _:A} cubical_set: CubicalSet uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] face-forall: (∀ phi) face-0: 0(𝔽) member: t ∈ T subtype_rel: A ⊆B all: x:A. B[x] names: names(I) uimplies: supposing a nat: so_lambda: λ2x.t[x] so_apply: x[s] prop: squash: T bdd-distributive-lattice: BoundedDistributiveLattice and: P ∧ Q cubical-type-at: A(a) pi1: fst(t) face-type: 𝔽 constant-cubical-type: (X) I_cube: A(I) functor-ob: ob(F) face-presheaf: 𝔽 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 implies:  Q bool: 𝔹 unit: Unit it: uiff: uiff(P;Q) exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False true: True iff: ⇐⇒ Q rev_implies:  Q not: ¬A nequal: a ≠ b ∈  satisfiable_int_formula: satisfiable_int_formula(fmla) cc-adjoin-cube: (v;u) cc-snd: q face-zero: (i=0) cubical-term-at: u(a) pi2: snd(t) DeMorgan-algebra: DeMorganAlgebra
Lemmas referenced :  fl_all-fl0 new-name_wf trivial-member-add-name1 fset-member_wf nat_wf int-deq_wf strong-subtype-deq-subtype strong-subtype-set3 le_wf istype-int strong-subtype-self add-name_wf equal_wf squash_wf true_wf istype-universe lattice-point_wf face_lattice_wf subtype_rel_set bounded-lattice-structure_wf lattice-structure_wf lattice-axioms_wf bounded-lattice-structure-subtype bounded-lattice-axioms_wf lattice-meet_wf lattice-join_wf eq_int_wf eqtt_to_assert assert_of_eq_int lattice-0_wf subtype_rel_self cubical-type-at_wf_face-type eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot neg_assert_of_eq_int eq_int_eq_true btrue_wf iff_weakening_equal not_assert_elim btrue_neq_bfalse full-omega-unsat intformnot_wf intformeq_wf itermVar_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_wf I_cube_wf fset_wf cubical-term-equal face-type_wf face-0_wf cubical_set_wf fl_all_wf istype-nat dM-to-FL-opp dM-to-FL_wf dM_wf DeMorgan-algebra-structure_wf DeMorgan-algebra-structure-subtype subtype_rel_transitivity DeMorgan-algebra-axioms_wf neg-dM_inc
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut equalitySymmetry functionExtensionality sqequalRule introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality lambdaEquality_alt setElimination rename inhabitedIsType equalityTransitivity dependent_functionElimination because_Cache dependent_set_memberEquality_alt universeIsType intEquality independent_isectElimination natural_numberEquality hyp_replacement imageElimination instantiate universeEquality productEquality cumulativity isectEquality lambdaFormation_alt unionElimination equalityElimination productElimination Error :memTop,  dependent_pairFormation_alt equalityIstype promote_hyp independent_functionElimination voidElimination imageMemberEquality baseClosed approximateComputation int_eqEquality

Latex:
\mforall{}[Gamma:j\mvdash{}].  ((Gamma  \mvdash{}  \mforall{}  (q=0))  =  0(\mBbbF{}))



Date html generated: 2020_05_20-PM-02_50_35
Last ObjectModification: 2020_04_04-PM-05_04_58

Theory : cubical!type!theory


Home Index