---

Step * of Lemma psc-restriction-id

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[I:cat-ob(C)]. ∀[s:X(I)].  (cat-id(C) I(s) = s ∈ X(I))
BY
{ (Auto
   THEN (Assert X ∈ ps_context{j:l}(C) BY
               Trivial)
   THEN DContext 2
   THEN RepUR ``psc-restriction`` 0
   THEN All Reduce
   THEN Auto
   THEN DCat 1
   THEN All (RepUR ``op-cat type-cat cat-id``)
   THEN RWO "9" 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[I:cat-ob(C)].  \mforall{}[s:X(I)].    (cat-id(C)  I(s)  =  s)


By

---

Latex:
(Auto
  THEN  (Assert  X  \mmember{}  ps\_context\{j:l\}(C)  BY
                          Trivial)
  THEN  DContext  2
  THEN  RepUR  ``psc-restriction``  0
  THEN  All  Reduce
  THEN  Auto
  THEN  DCat  1
  THEN  All  (RepUR  ``op-cat  type-cat  cat-id``)
  THEN  RWO  "9"  0
  THEN  Auto)

---

Home Index