Nuprl Lemma : csm-cubical-sigma

X,Delta:CubicalSet. ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀s:Delta ⟶ X.  ((Σ B)s = Σ (A)s (B)(s p;q) ∈ {Delta ⊢ _})


Proof




Definitions occuring in Statement :  cubical-sigma: Σ B csm-adjoin: (s;u) cc-snd: q cc-fst: p cube-context-adjoin: X.A csm-ap-type: (AF)s cubical-type: {X ⊢ _} csm-comp: F cube-set-map: A ⟶ B cubical-set: CubicalSet all: x:A. B[x] equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a cubical-type: {X ⊢ _} cube-set-map: A ⟶ B nat-trans: nat-trans(C;D;F;G) csm-ap-type: (AF)s cubical-sigma: Σ B cubical-type-at: A(a) pi1: fst(t) and: P ∧ Q top: Top cubical-type-ap-morph: (u f) pi2: snd(t) subtype_rel: A ⊆B cc-adjoin-cube: (v;u) cc-snd: q csm-ap: (s)x cc-fst: p csm-comp: F type-cat: TypeCat cat-comp: cat-comp(C) compose: g cube-context-adjoin: X.A I-cube: X(I) functor-ob: ob(F) cat-arrow: cat-arrow(C) name-cat: NameCat cat-ob: cat-ob(C) squash: T prop: true: True guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q csm-adjoin: (s;u) trans-comp: t1 t2 so_lambda: λ2x.t[x] so_apply: x[s] functor-arrow: arrow(F) cube-set-restriction: f(s)
Lemmas referenced :  cubical-type-equal csm-ap-type_wf cubical-sigma_wf cube-set-map_wf cubical-type_wf cube-context-adjoin_wf cubical-set_wf csm-ap_wf csm-adjoin-ap istype-void I-cube_wf list_wf coordinate_name_wf cc-adjoin-cube_wf subtype_rel_self cubical-type-at_wf name-morph_wf cube-set-restriction_wf trans_comp_ap_lemma ob_pair_lemma cat_comp_tuple_lemma subtype_rel-equal equal_wf squash_wf true_wf istype-universe csm-ap-restriction iff_weakening_equal ap_mk_nat_trans_lemma cc-adjoin-cube-restriction
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis equalityTransitivity equalitySymmetry independent_isectElimination universeIsType inhabitedIsType setElimination rename productElimination sqequalRule dependent_pairEquality_alt lambdaEquality_alt productEquality applyEquality isect_memberEquality_alt voidElimination functionExtensionality because_Cache dependent_functionElimination functionIsType instantiate imageElimination universeEquality natural_numberEquality imageMemberEquality baseClosed independent_functionElimination applyLambdaEquality dependent_set_memberEquality_alt independent_pairFormation productIsType equalityIsType1

Latex:
\mforall{}X,Delta:CubicalSet.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}B:\{X.A  \mvdash{}  \_\}.  \mforall{}s:Delta  {}\mrightarrow{}  X.    ((\mSigma{}  A  B)s  =  \mSigma{}  (A)s  (B)(s  o  p;q))



Date html generated: 2019_11_05-PM-00_26_42
Last ObjectModification: 2018_11_10-PM-03_06_05

Theory : cubical!sets


Home Index