Nuprl Lemma : csm-ap-restriction

X,Y:CubicalSet. ∀s:X ⟶ Y. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X(I).  (f((s)a) (s)f(a) ∈ Y(J))


Proof




Definitions occuring in Statement :  cube-set-restriction: f(s) csm-ap: (s)x I-cube: X(I) cube-set-map: A ⟶ B cubical-set: CubicalSet name-morph: name-morph(I;J) coordinate_name: Cname list: List all: x:A. B[x] equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] cubical-set: CubicalSet cube-set-map: A ⟶ B nat-trans: nat-trans(C;D;F;G) I-cube: X(I) functor-ob: functor-ob(F) pi1: fst(t) functor-arrow: functor-arrow(F) type-cat: TypeCat cat-comp: cat-comp(C) cat-arrow: cat-arrow(C) name-cat: NameCat cat-ob: cat-ob(C) pi2: snd(t) compose: g cube-set-restriction: f(s) csm-ap: (s)x member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  I-cube_wf name-morph_wf list_wf coordinate_name_wf cube-set-map_wf cubical-set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution setElimination thin rename productElimination sqequalRule hypothesis dependent_functionElimination hypothesisEquality applyEquality lambdaEquality functionEquality lemma_by_obid isectElimination

Latex:
\mforall{}X,Y:CubicalSet.  \mforall{}s:X  {}\mrightarrow{}  Y.  \mforall{}I,J:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}a:X(I).    (f((s)a)  =  (s)f(a))



Date html generated: 2016_06_16-PM-05_37_36
Last ObjectModification: 2015_12_28-PM-04_37_11

Theory : cubical!sets


Home Index