---

Step * 1 2 of Lemma groupoids_wf

.....wf..... 
λG,H,K,F,G. functor-comp(F;G) ∈ x:Groupoid
⟶ y:Groupoid
⟶ z:Groupoid
⟶ groupoid-map(x;y)
⟶ groupoid-map(y;z)
⟶ groupoid-map(x;z)
BY
{ (Auto THEN D -2 THEN D -1 THEN MemTypeCD THEN Auto THEN RepUR ``functor-comp`` 0 THEN (RWW "5 7" 0 THENA Auto)) }

---

Latex:

---

Latex:
.....wf..... 
\mlambda{}G,H,K,F,G.  functor-comp(F;G)  \mmember{}  x:Groupoid
{}\mrightarrow{}  y:Groupoid
{}\mrightarrow{}  z:Groupoid
{}\mrightarrow{}  groupoid-map(x;y)
{}\mrightarrow{}  groupoid-map(y;z)
{}\mrightarrow{}  groupoid-map(x;z)


By

---

Latex:
(Auto
  THEN  D  -2
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto
  THEN  RepUR  ``functor-comp``  0
  THEN  (RWW  "5  7"  0  THENA  Auto))

---

Home Index