---

Step * of Lemma ext-eq-psc_wf

No Annotations
∀[C:SmallCategory]. ∀[X,Y:ps_context{j:l}(C)].  (X ≡ Y ∈ ℙ{[i | j']})
BY
{ (Intros
   THEN Unhide
   THEN Unfold `ext-eq-psc` 0
   THEN RepUR ``ext-equal-presheaves`` 0
   THEN ((RepeatFor 2 (D 1) THEN D 2 THEN D 3) THEN RepeatFor 2 (DVar `X') THEN RepeatFor 2 (DVar `Y'))
   THEN All (RepUR ``cat-ob cat-arrow cat-comp op-cat type-cat``)
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X,Y:ps\_context\{j:l\}(C)].    (X  \mequiv{}  Y  \mmember{}  \mBbbP{}\{[i  |  j']\})


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  Unfold  `ext-eq-psc`  0
  THEN  RepUR  ``ext-equal-presheaves``  0
  THEN  ((RepeatFor  2  (D  1)  THEN  D  2  THEN  D  3)
              THEN  RepeatFor  2  (DVar  `X')
              THEN  RepeatFor  2  (DVar  `Y'))
  THEN  All  (RepUR  ``cat-ob  cat-arrow  cat-comp  op-cat  type-cat``)
  THEN  Auto)

---

Home Index