---

Step * of Lemma groupoids_wf

Groupoids ∈ SmallCategory'
BY
{ Unfold `groupoids` 0 }

1
Cat(ob = Groupoid;
    arrow(G,H) = groupoid-map(G;H);
    id(G) = 1;
    comp(G,H,K,F,G) = functor-comp(F;G)) ∈ SmallCategory'

---

Latex:

---

Latex:
Groupoids  \mmember{}  SmallCategory'


By

---

Latex:
Unfold  `groupoids`  0

---

Home Index