---

Step * of Lemma functor-comp-id

∀[A,B:SmallCategory]. ∀[F:Functor(A;B)].
  ((functor-comp(F;1) = F ∈ Functor(A;B)) ∧ (functor-comp(1;F) = F ∈ Functor(A;B)))
BY
{ (Auto THEN (BLemma `equal-functors` THENA Auto) THEN RepUR ``id_functor functor-comp`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:SmallCategory].  \mforall{}[F:Functor(A;B)].    ((functor-comp(F;1)  =  F)  \mwedge{}  (functor-comp(1;F)  =  F))


By

---

Latex:
(Auto  THEN  (BLemma  `equal-functors`  THENA  Auto)  THEN  RepUR  ``id\_functor  functor-comp``  0  THEN  Auto)

---

Home Index