---

Step * of Lemma pscm-ap_wf

No Annotations
∀[C:SmallCategory]. ∀[X,Y:ps_context{j:l}(C)]. ∀[s:psc_map{j:l}(C; X; Y)]. ∀[I:cat-ob(C)]. ∀[x:X(I)].  ((s)x ∈ Y(I))
BY
{ (Auto
   THEN Unfold `pscm-ap` 0
   THEN (RepeatFor 2 (D 2) THEN RepeatFor 2 (D 5))
   THEN All Reduce
   THEN All (RepUR ``I_set functor-ob psc_map``)
   THEN D -3
   THEN DCat 1
   THEN RepUR ``cat-ob op-cat cat-arrow functor-ob type-cat`` -4
   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:cat-ob(C)].
\mforall{}[x:X(I)].
    ((s)x  \mmember{}  Y(I))


By

---

Latex:
(Auto
  THEN  Unfold  `pscm-ap`  0
  THEN  (RepeatFor  2  (D  2)  THEN  RepeatFor  2  (D  5))
  THEN  All  Reduce
  THEN  All  (RepUR  ``I\_set  functor-ob  psc\_map``)
  THEN  D  -3
  THEN  DCat  1
  THEN  RepUR  ``cat-ob  op-cat  cat-arrow  functor-ob  type-cat``  -4
  THEN  Auto)

---

Home Index