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

`∀X,Delta:CubicalSet. ∀s:Delta ⟶ X. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:Delta(I). ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}.`
`∀w:cubical-pi-family(X;A;B;I;(s)a).`
`  (λK,g. (w K (f o g)) ∈ cubical-pi-family(X;A;B;J;(s)f(a)))`

Proof

Definitions occuring in Statement :  cubical-pi-family: `cubical-pi-family(X;A;B;I;a)` cube-context-adjoin: `X.A` cubical-type: `{X ⊢ _}` cube-set-restriction: `f(s)` csm-ap: `(s)x` I-cube: `X(I)` cube-set-map: `A ⟶ B` cubical-set: `CubicalSet` name-comp: `(f o g)` name-morph: `name-morph(I;J)` coordinate_name: `Cname` list: `T List` all: `∀x:A. B[x]` member: `t ∈ T` apply: `f a` lambda: `λx.A[x]`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` cubical-pi-family: `cubical-pi-family(X;A;B;I;a)` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` squash: `↓T` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` true: `True` top: `Top` cubical-type-ap-morph: `(u a f)` cand: `A c∧ B` cubical-type: `{X ⊢ _}` pi2: `snd(t)` prop: `ℙ` cubical-type-at: `A(a)` pi1: `fst(t)`
Lemmas referenced :  list_wf coordinate_name_wf name-comp_wf subtype_rel_dep_function cubical-type-at_wf cube-set-restriction_wf csm-ap_wf cube-context-adjoin_wf cc-adjoin-cube_wf subtype_rel-equal equal_wf I-cube_wf csm-ap-restriction iff_weakening_equal cube-set-restriction-comp name-morph_wf cubical-type-ap-morph_wf cc-adjoin-cube-restriction all_wf cubical-pi-family_wf cubical-type_wf cube-set-map_wf squash_wf true_wf subtype_rel_self cubical-set_wf name-comp-assoc and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution setElimination thin rename dependent_set_memberEquality lambdaEquality applyEquality functionExtensionality hypothesisEquality introduction extract_by_obid isectElimination hypothesis because_Cache sqequalRule dependent_functionElimination independent_isectElimination imageElimination imageMemberEquality baseClosed equalityTransitivity equalitySymmetry productElimination independent_functionElimination natural_numberEquality isect_memberEquality voidElimination voidEquality independent_pairFormation universeEquality instantiate hyp_replacement functionEquality applyLambdaEquality

Latex:
\mforall{}X,Delta:CubicalSet.  \mforall{}s:Delta  {}\mrightarrow{}  X.  \mforall{}I,J:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}a:Delta(I).  \mforall{}A:\{X  \mvdash{}  \_\}.
\mforall{}B:\{X.A  \mvdash{}  \_\}.  \mforall{}w:cubical-pi-family(X;A;B;I;(s)a).
(\mlambda{}K,g.  (w  K  (f  o  g))  \mmember{}  cubical-pi-family(X;A;B;J;(s)f(a)))

Date html generated: 2018_05_23-PM-06_29_38
Last ObjectModification: 2018_05_20-PM-04_11_33

Theory : cubical!sets

Home Index