---

Step * of 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))
BY
{ (Auto
   THEN RepeatFor 2 (D 2)
   THEN (RepeatFor 2 (D 1) THEN All Reduce)
   THEN DVar `s'
   THEN All (RepUR ``cat-ob cat-comp name-cat cat-arrow compose 
                     cube-set-restriction csm-ap I-cube
                     type-cat functor-ob functor-arrow``)⋅
   THEN (InstHyp [⌜I⌝;⌜J⌝; ⌜f⌝] (-5)⋅ THENA Auto)
   THEN (ApFunToHypEquands `Z' ⌜Z a⌝ ⌜X1 J⌝ (-1)⋅ THENM Reduce (-1))
   THEN Auto) }

---

Latex:

---

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))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  2)
  THEN  (RepeatFor  2  (D  1)  THEN  All  Reduce)
  THEN  DVar  `s'
  THEN  All  (RepUR  ``cat-ob  cat-comp  name-cat  cat-arrow  compose 
                                      cube-set-restriction  csm-ap  I-cube
                                      type-cat  functor-ob  functor-arrow``)\mcdot{}
  THEN  (InstHyp  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}Z  a\mkleeneclose{}  \mkleeneopen{}X1  J\mkleeneclose{}  (-1)\mcdot{}  THENM  Reduce  (-1))
  THEN  Auto)

---

Home Index