---

Step * of Lemma pscm-ap-restriction

No Annotations
∀C:SmallCategory. ∀X,Y:ps_context{j:l}(C). ∀s:psc_map{j:l}(C; X; Y). ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I).
  (f((s)a) = (s)f(a) ∈ Y(J))
BY
{ (Auto
   THEN DContext 3
   THEN DContext 2
   THEN DVar `s'
   THEN DCat 1
   THEN All (RepUR ``cat-ob cat-comp op-cat cat-arrow compose 
                     psc-restriction pscm-ap I_set
                     type-cat functor-ob functor-arrow``)⋅
   THEN (InstHyp [⌜I⌝;⌜J⌝; ⌜f⌝] (-5)⋅ THENA Auto)
   THEN (ApFunToHypEquands `Z' ⌜Z a⌝ ⌜F J⌝ (-1)⋅ THENM Reduce (-1))
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}C:SmallCategory.  \mforall{}X,Y:ps\_context\{j:l\}(C).  \mforall{}s:psc\_map\{j:l\}(C;  X;  Y).  \mforall{}I,J:cat-ob(C).
\mforall{}f:cat-arrow(C)  J  I.  \mforall{}a:X(I).
    (f((s)a)  =  (s)f(a))


By

---

Latex:
(Auto
  THEN  DContext  3
  THEN  DContext  2
  THEN  DVar  `s'
  THEN  DCat  1
  THEN  All  (RepUR  ``cat-ob  cat-comp  op-cat  cat-arrow  compose 
                                      psc-restriction  pscm-ap  I\_set
                                      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{}F  J\mkleeneclose{}  (-1)\mcdot{}  THENM  Reduce  (-1))
  THEN  Auto)

---

Home Index