---

Step * 1 of Lemma cat-cat_wf


Cat ∈ ob:𝕌'
× arrow:ob ⟶ ob ⟶ 𝕌'
× x:ob ⟶ (arrow x x)
× (x:ob ⟶ y:ob ⟶ z:ob ⟶ (arrow x y) ⟶ (arrow y z) ⟶ (arrow x z))
BY
{ (RepUR ``cat-cat`` 0
   THEN RepeatFor 2 ((MemCD THENL [Auto; Reduce 0; Auto]))
   THEN RepeatFor 2 (MemCD)
   THEN Try (RepeatFor 4 (MemCD'))
   THEN Auto) }

---

Latex:

---

Latex:

Cat  \mmember{}  ob:\mBbbU{}'
\mtimes{}  arrow:ob  {}\mrightarrow{}  ob  {}\mrightarrow{}  \mBbbU{}'
\mtimes{}  x:ob  {}\mrightarrow{}  (arrow  x  x)
\mtimes{}  (x:ob  {}\mrightarrow{}  y:ob  {}\mrightarrow{}  z:ob  {}\mrightarrow{}  (arrow  x  y)  {}\mrightarrow{}  (arrow  y  z)  {}\mrightarrow{}  (arrow  x  z))


By

---

Latex:
(RepUR  ``cat-cat``  0
  THEN  RepeatFor  2  ((MemCD  THENL  [Auto;  Reduce  0;  Auto]))
  THEN  RepeatFor  2  (MemCD)
  THEN  Try  (RepeatFor  4  (MemCD'))
  THEN  Auto)

---

Home Index