---

Step * 1 4 of Lemma groupoids_wf


∀G,H,z,K:Groupoid. ∀F:groupoid-map(G;H). ∀G1:groupoid-map(H;z). ∀h:groupoid-map(z;K).
  (functor-comp(functor-comp(F;G1);h) = functor-comp(F;functor-comp(G1;h)) ∈ groupoid-map(G;K))
BY
{ (Intros
   THEN D -3
   THEN D -2
   THEN D -1
   THEN EqTypeCD
   THEN Auto
   THEN RepUR ``functor-comp`` 0
   THEN RWW "6 8 10" 0
   THEN Auto) }

---

Latex:

---

Latex:

\mforall{}G,H,z,K:Groupoid.  \mforall{}F:groupoid-map(G;H).  \mforall{}G1:groupoid-map(H;z).  \mforall{}h:groupoid-map(z;K).
    (functor-comp(functor-comp(F;G1);h)  =  functor-comp(F;functor-comp(G1;h)))


By

---

Latex:
(Intros
  THEN  D  -3
  THEN  D  -2
  THEN  D  -1
  THEN  EqTypeCD
  THEN  Auto
  THEN  RepUR  ``functor-comp``  0
  THEN  RWW  "6  8  10"  0
  THEN  Auto)

---

Home Index