---

Step * 1 1 of Lemma groupoids_wf

.....wf..... 
λG.1 ∈ x:Groupoid ⟶ groupoid-map(x;x)
BY
{ ((MemCD THENA Auto) THEN MemTypeCD THEN Auto THEN RepUR ``id_functor`` 0 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
\mlambda{}G.1  \mmember{}  x:Groupoid  {}\mrightarrow{}  groupoid-map(x;x)


By

---

Latex:
((MemCD  THENA  Auto)  THEN  MemTypeCD  THEN  Auto  THEN  RepUR  ``id\_functor``  0  THEN  Auto)

---

Home Index