Nuprl Lemma : face-forall-and

[Gamma:j⊢]. ∀[phi,psi:{Gamma.𝕀 ⊢ _:𝔽}].  ((Gamma ⊢ ∀ (phi ∧ psi)) ((∀ phi) ∧ (∀ psi)) ∈ {Gamma ⊢ _:𝔽})


Proof




Definitions occuring in Statement :  face-forall: (∀ phi) face-and: (a ∧ b) face-type: 𝔽 interval-type: 𝕀 cube-context-adjoin: X.A cubical-term: {X ⊢ _:A} cubical_set: CubicalSet uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B uimplies: supposing a interval-presheaf: 𝕀 all: x:A. B[x] names: names(I) nat: so_lambda: λ2x.t[x] so_apply: x[s] prop: face-forall: (∀ phi) face-and: (a ∧ b) cubical-term-at: u(a) cubical-term: {X ⊢ _:A} 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 cubical-type-at: A(a) pi1: fst(t) face-type: 𝔽 constant-cubical-type: (X) I_cube: A(I) functor-ob: ob(F) face-presheaf: 𝔽
Lemmas referenced :  I_cube_wf fset_wf nat_wf cubical-term-equal face-type_wf face-forall_wf face-and_wf cube-context-adjoin_wf interval-type_wf cubical-term_wf cubical_set_cumulativity-i-j cubical_set_wf interval-type-at I_cube_pair_redex_lemma dM_inc_wf add-name_wf new-name_wf trivial-member-add-name1 fset-member_wf int-deq_wf strong-subtype-deq-subtype strong-subtype-set3 le_wf istype-int strong-subtype-self fl_all-meet cc-adjoin-cube_wf cube-set-restriction_wf nc-s_wf f-subset-add-name subtype_rel_self cubical-type-at_wf_face-type
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut functionExtensionality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis instantiate applyEquality because_Cache sqequalRule equalityTransitivity equalitySymmetry independent_isectElimination inhabitedIsType isect_memberEquality_alt axiomEquality isectIsTypeImplies universeIsType Error :memTop,  dependent_functionElimination dependent_set_memberEquality_alt lambdaEquality_alt setElimination rename intEquality natural_numberEquality

Latex:
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[phi,psi:\{Gamma.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}].    ((Gamma  \mvdash{}  \mforall{}  (phi  \mwedge{}  psi))  =  ((\mforall{}  phi)  \mwedge{}  (\mforall{}  psi)))



Date html generated: 2020_05_20-PM-02_51_11
Last ObjectModification: 2020_04_04-PM-05_05_52

Theory : cubical!type!theory


Home Index