Nuprl Lemma : face-term-implies-and

[Gamma:j⊢]. ∀[a,b,c:{Gamma ⊢ _:𝔽}].  (Gamma ⊢ (c  (a ∧ b))) supposing (Gamma ⊢ (c  a) and Gamma ⊢ (c  b))


Proof




Definitions occuring in Statement :  face-term-implies: Gamma ⊢ (phi  psi) face-and: (a ∧ b) face-type: 𝔽 cubical-term: {X ⊢ _:A} cubical_set: CubicalSet uimplies: supposing a uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a face-term-implies: Gamma ⊢ (phi  psi) all: x:A. B[x] implies:  Q cubical-term-at: u(a) subtype_rel: A ⊆B bdd-distributive-lattice: BoundedDistributiveLattice so_lambda: λ2x.t[x] prop: and: P ∧ Q so_apply: x[s] 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 iff: ⇐⇒ Q rev_implies:  Q cand: c∧ B guard: {T}
Lemmas referenced :  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 equal_wf lattice-meet_wf lattice-join_wf cubical-term-at_wf face-type_wf subtype_rel_self lattice-1_wf I_cube_wf fset_wf nat_wf face-term-implies_wf cubical-term_wf cubical_set_wf face-and-eq-1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut lambdaFormation_alt sqequalHypSubstitution hypothesis equalityIstype universeIsType extract_by_obid isectElimination thin hypothesisEquality applyEquality sqequalRule instantiate lambdaEquality_alt productEquality cumulativity isectEquality because_Cache independent_isectElimination setElimination rename inhabitedIsType equalityTransitivity equalitySymmetry dependent_functionElimination axiomEquality functionIsTypeImplies isect_memberEquality_alt isectIsTypeImplies productElimination independent_functionElimination independent_pairFormation

Latex:
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[a,b,c:\{Gamma  \mvdash{}  \_:\mBbbF{}\}].
    (Gamma  \mvdash{}  (c  {}\mRightarrow{}  (a  \mwedge{}  b)))  supposing  (Gamma  \mvdash{}  (c  {}\mRightarrow{}  a)  and  Gamma  \mvdash{}  (c  {}\mRightarrow{}  b))



Date html generated: 2020_05_20-PM-02_48_08
Last ObjectModification: 2020_04_04-PM-05_02_15

Theory : cubical!type!theory


Home Index