---

Step * of Lemma small-category-subtype

SmallCategory ⊆r SmallCategory'
BY
{ ((D 0 THENA Auto)
   THEN D -1
   THEN RepeatFor 3 (D -2)
   THEN Reduce (-1)
   THEN (Unfold `small-category` 0 THEN At ⌜𝕌'⌝ MemTypeCD⋅ THEN Reduce 0 THEN Auto)) }

---

Latex:

---

Latex:
SmallCategory  \msubseteq{}r  SmallCategory'


By

---

Latex:
((D  0  THENA  Auto)
  THEN  D  -1
  THEN  RepeatFor  3  (D  -2)
  THEN  Reduce  (-1)
  THEN  (Unfold  `small-category`  0  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  MemTypeCD\mcdot{}  THEN  Reduce  0  THEN  Auto))

---

Home Index