Nuprl Lemma : interval-rev_wf

[Gamma:j⊢]. ∀[r:{Gamma ⊢ _:𝕀}].  (1-(r) ∈ {Gamma ⊢ _:𝕀})


Proof




Definitions occuring in Statement :  interval-rev: 1-(r) interval-type: 𝕀 cubical-term: {X ⊢ _:A} cubical_set: CubicalSet uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T cubical-term: {X ⊢ _:A} interval-rev: 1-(r) subtype_rel: A ⊆B DeMorgan-algebra: DeMorganAlgebra cubical-type-at: A(a) pi1: fst(t) interval-type: 𝕀 constant-cubical-type: (X) I_cube: A(I) functor-ob: ob(F) interval-presheaf: 𝕀 lattice-point: Point(l) record-select: r.x dM: dM(I) free-DeMorgan-algebra: free-DeMorgan-algebra(T;eq) mk-DeMorgan-algebra: mk-DeMorgan-algebra(L;n) record-update: r[x := v] ifthenelse: if then else fi  eq_atom: =a y bfalse: ff free-DeMorgan-lattice: free-DeMorgan-lattice(T;eq) free-dist-lattice: free-dist-lattice(T; eq) mk-bounded-distributive-lattice: mk-bounded-distributive-lattice mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o) btrue: tt so_lambda: λ2x.t[x] prop: and: P ∧ Q guard: {T} uimplies: supposing a so_apply: x[s] all: x:A. B[x] true: True squash: T iff: ⇐⇒ Q rev_implies:  Q implies:  Q
Lemmas referenced :  dma-neg_wf dM_wf cubical-term-at_wf interval-type_wf subtype_rel_self lattice-point_wf subtype_rel_set DeMorgan-algebra-structure_wf lattice-structure_wf lattice-axioms_wf bounded-lattice-structure-subtype DeMorgan-algebra-structure-subtype subtype_rel_transitivity bounded-lattice-structure_wf bounded-lattice-axioms_wf equal_wf lattice-meet_wf lattice-join_wf DeMorgan-algebra-axioms_wf cubical-type-at_wf I_cube_wf fset_wf nat_wf names-hom_wf istype-cubical-type-at cube-set-restriction_wf cubical-type-ap-morph_wf cubical-term_wf cubical_set_wf squash_wf true_wf istype-universe cubical-term-at-morph iff_weakening_equal dM-lift-neg interval-type-ap-morph
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut dependent_set_memberEquality_alt lambdaEquality_alt extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality setElimination rename inhabitedIsType equalityTransitivity equalitySymmetry sqequalRule instantiate productEquality cumulativity because_Cache independent_isectElimination isectEquality universeIsType lambdaFormation_alt functionIsType equalityIstype axiomEquality isect_memberEquality_alt isectIsTypeImplies natural_numberEquality imageElimination universeEquality imageMemberEquality baseClosed productElimination independent_functionElimination Error :memTop

Latex:
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[r:\{Gamma  \mvdash{}  \_:\mBbbI{}\}].    (1-(r)  \mmember{}  \{Gamma  \mvdash{}  \_:\mBbbI{}\})



Date html generated: 2020_05_20-PM-02_36_50
Last ObjectModification: 2020_04_04-AM-10_11_07

Theory : cubical!type!theory


Home Index