Nuprl Lemma : context-adjoin-subset0

[H:j⊢]. ∀[phi:{H ⊢ _:𝔽}].  ∀T:{H ⊢ _}. sub_cubical_set{k:l}(H.T, (phi)p; H, phi.T)


Proof




Definitions occuring in Statement :  context-subset: Gamma, phi face-type: 𝔽 cc-fst: p cube-context-adjoin: X.A csm-ap-term: (t)s cubical-term: {X ⊢ _:A} cubical-type: {X ⊢ _} sub_cubical_set: Y ⊆ X cubical_set: CubicalSet uall: [x:A]. B[x] all: x:A. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] sub_cubical_set: Y ⊆ X member: t ∈ T cubical-term: {X ⊢ _:A} cc-fst: p csm-ap-term: (t)s cubical-term-at: u(a) csm-ap: (s)x subtype_rel: A ⊆B bdd-distributive-lattice: BoundedDistributiveLattice so_lambda: λ2x.t[x] prop: and: P ∧ Q so_apply: x[s] uimplies: supposing a 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 cube_set_map: A ⟶ B psc_map: A ⟶ B nat-trans: nat-trans(C;D;F;G) csm-id: 1(X) cat-arrow: cat-arrow(C) op-cat: op-cat(C) cat-ob: cat-ob(C) cube-cat: CubeCat spreadn: spread4 cube-context-adjoin: X.A type-cat: TypeCat pi2: snd(t) context-subset: Gamma, phi functor-arrow: arrow(F) cat-comp: cat-comp(C) compose: g guard: {T} squash: T true: True iff: ⇐⇒ Q rev_implies:  Q implies:  Q
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 pi1_wf_top I_cube_wf istype-cubical-type-at fset_wf nat_wf I_cube_pair_redex_lemma cube_set_restriction_pair_lemma cubical-type_wf cubical-term_wf face-type_wf cubical_set_wf cubical-term-at_wf subtype_rel_self cubical-type-at_wf lattice-1_wf squash_wf true_wf istype-universe face-term-at-restriction-eq-1 iff_weakening_equal cube-set-restriction_wf cubical-type-ap-morph_wf names-hom_wf pi2_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt cut sqequalHypSubstitution setElimination thin rename sqequalRule introduction extract_by_obid isectElimination hypothesisEquality hypothesis applyEquality instantiate lambdaEquality_alt productEquality cumulativity isectEquality because_Cache universeIsType independent_isectElimination productElimination independent_pairEquality Error :memTop,  equalityTransitivity equalitySymmetry hyp_replacement productIsType dependent_set_memberEquality_alt dependent_functionElimination dependent_pairEquality_alt equalityIstype inhabitedIsType setIsType functionExtensionality imageElimination universeEquality natural_numberEquality imageMemberEquality baseClosed independent_functionElimination setEquality functionIsType

Latex:
\mforall{}[H:j\mvdash{}].  \mforall{}[phi:\{H  \mvdash{}  \_:\mBbbF{}\}].    \mforall{}T:\{H  \mvdash{}  \_\}.  sub\_cubical\_set\{k:l\}(H.T,  (phi)p;  H,  phi.T)



Date html generated: 2020_05_20-PM-03_04_43
Last ObjectModification: 2020_04_13-PM-05_43_31

Theory : cubical!type!theory


Home Index