---

Step * 1 of Lemma discrete-groupoid_wf


1. X : Type
2. x : cat-ob(discrete-cat(X))
3. y : cat-ob(discrete-cat(X))
4. f : cat-arrow(discrete-cat(X)) x y
⊢ ⋅ ∈ cat-arrow(discrete-cat(X)) y x
BY
{ (All (RepUR ``discrete-cat mk-cat``) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  X  :  Type
2.  x  :  cat-ob(discrete-cat(X))
3.  y  :  cat-ob(discrete-cat(X))
4.  f  :  cat-arrow(discrete-cat(X))  x  y
\mvdash{}  \mcdot{}  \mmember{}  cat-arrow(discrete-cat(X))  y  x


By

---

Latex:
(All  (RepUR  ``discrete-cat  mk-cat``)  THEN  Auto)\mcdot{}

---

Home Index