### Nuprl Lemma : csm-adjoin-fst-snd

`∀[Gamma,Delta:CubicalSet]. ∀[A:{Gamma ⊢ _}].  ((p;q) = 1(Gamma.A) ∈ Gamma.A ⟶ Gamma.A)`

Proof

Definitions occuring in Statement :  csm-adjoin: `(s;u)` cc-snd: `q` cc-fst: `p` cube-context-adjoin: `X.A` cubical-type: `{X ⊢ _}` csm-id: `1(X)` cube-set-map: `A ⟶ B` cubical-set: `CubicalSet` uall: `∀[x:A]. B[x]` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` uimplies: `b supposing a` cubical-type: `{X ⊢ _}` cc-snd: `q` cc-fst: `p` csm-adjoin: `(s;u)` cube-context-adjoin: `X.A` csm-id: `1(X)` I-cube: `X(I)` all: `∀x:A. B[x]` top: `Top` csm-ap: `(s)x` functor-ob: `ob(F)` type-cat: `TypeCat` identity-trans: `identity-trans(C;D;F)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` and: `P ∧ Q` squash: `↓T` prop: `ℙ` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` pi1: `fst(t)` pi2: `snd(t)` cubical-type-at: `A(a)`
Lemmas referenced :  cubical-type_wf cubical-set_wf cube-context-adjoin_wf csm-id_wf csm-adjoin_wf cc-fst_wf cc-snd_wf cube-set-map-subtype csm-equal ob_pair_lemma cat_id_tuple_lemma ap_mk_nat_trans_lemma I-cube_wf cubical-type-at_wf list_wf coordinate_name_wf name-morph_wf cube-set-restriction_wf all_wf equal_wf id-morph_wf subtype_rel-equal squash_wf true_wf cube-set-restriction-id iff_weakening_equal name-comp_wf cube-set-restriction-comp
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut equalitySymmetry hypothesis extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule isect_memberEquality axiomEquality because_Cache applyEquality independent_isectElimination setElimination rename productElimination dependent_functionElimination voidElimination voidEquality functionExtensionality productEquality dependent_set_memberEquality dependent_pairEquality functionEquality lambdaEquality instantiate imageElimination equalityTransitivity universeEquality natural_numberEquality imageMemberEquality baseClosed independent_functionElimination

Latex:
\mforall{}[Gamma,Delta:CubicalSet].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].    ((p;q)  =  1(Gamma.A))

Date html generated: 2017_10_05-AM-10_13_43
Last ObjectModification: 2017_07_28-AM-11_19_04

Theory : cubical!sets

Home Index