Nuprl Lemma : face-0-or

[X:j⊢]. ∀[psi:{X ⊢ _:𝔽}].  ((0(𝔽) ∨ psi) psi ∈ {X ⊢ _:𝔽})


Proof




Definitions occuring in Statement :  face-or: (a ∨ b) face-0: 0(𝔽) face-type: 𝔽 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-0: 0(𝔽) face-or: (a ∨ b) cubical-term-at: u(a) member: t ∈ T subtype_rel: A ⊆B 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 bdd-distributive-lattice: BoundedDistributiveLattice so_lambda: λ2x.t[x] prop: and: P ∧ Q so_apply: x[s] uimplies: supposing a
Lemmas referenced :  lattice-join-0 face_lattice_wf bdd-distributive-lattice-subtype-bdd-lattice cubical-term-at_wf face-type_wf subtype_rel_self lattice-point_wf subtype_rel_set bounded-lattice-structure_wf lattice-structure_wf lattice-axioms_wf bounded-lattice-structure-subtype bounded-lattice-axioms_wf equal_wf lattice-meet_wf lattice-join_wf I_cube_wf fset_wf nat_wf cubical-term-equal face-or_wf face-0_wf cubical-term_wf cubical_set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut functionExtensionality sqequalRule introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality instantiate lambdaEquality_alt productEquality cumulativity isectEquality because_Cache universeIsType independent_isectElimination productElimination equalityTransitivity equalitySymmetry

Latex:
\mforall{}[X:j\mvdash{}].  \mforall{}[psi:\{X  \mvdash{}  \_:\mBbbF{}\}].    ((0(\mBbbF{})  \mvee{}  psi)  =  psi)



Date html generated: 2020_05_20-PM-02_41_58
Last ObjectModification: 2020_04_04-PM-04_50_11

Theory : cubical!type!theory


Home Index