### Nuprl Lemma : csm-cubical-pi-family

`∀X,Delta:CubicalSet. ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀s:Delta ⟶ X. ∀I:Cname List. ∀a:Delta(I).`
`  (cubical-pi-family(X;A;B;I;(s)a) = cubical-pi-family(Delta;(A)s;(B)(s o p;q);I;a) ∈ Type)`

Proof

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

Latex:
\mforall{}X,Delta:CubicalSet.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}B:\{X.A  \mvdash{}  \_\}.  \mforall{}s:Delta  {}\mrightarrow{}  X.  \mforall{}I:Cname  List.  \mforall{}a:Delta(I).
(cubical-pi-family(X;A;B;I;(s)a)  =  cubical-pi-family(Delta;(A)s;(B)(s  o  p;q);I;a))

Date html generated: 2019_11_05-PM-00_26_29
Last ObjectModification: 2018_11_10-PM-02_44_54

Theory : cubical!sets

Home Index