---

Step * of Lemma functor-comp-id

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

---

Latex:

---

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


By

---

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

---

Home Index