---

Step * 1 3 of Lemma groupoids_wf


∀G,H:Groupoid. ∀F:groupoid-map(G;H).
  ((functor-comp(1;F) = F ∈ groupoid-map(G;H)) ∧ (functor-comp(F;1) = F ∈ groupoid-map(G;H)))
BY
{ (Intros THEN D -1 THEN D 0 THEN Symmetry THEN EqTypeCD THEN Auto) }

---

Latex:

---

Latex:

\mforall{}G,H:Groupoid.  \mforall{}F:groupoid-map(G;H).    ((functor-comp(1;F)  =  F)  \mwedge{}  (functor-comp(F;1)  =  F))


By

---

Latex:
(Intros  THEN  D  -1  THEN  D  0  THEN  Symmetry  THEN  EqTypeCD  THEN  Auto)

---

Home Index