---

Step * of Lemma functor-arrow-id

∀[C,D:SmallCategory]. ∀[F:Functor(C;D)].
  ∀x:cat-ob(C)
    ((functor-arrow(F) x x (cat-id(C) x))
    = (cat-id(D) (functor-ob(F) x))
    ∈ (cat-arrow(D) (functor-ob(F) x) (functor-ob(F) x)))
BY
{ (Auto THEN OnVar `F' DFunctor THEN Reduce 0 THEN BackThruSomeHyp) }

---

Latex:

---

Latex:
\mforall{}[C,D:SmallCategory].  \mforall{}[F:Functor(C;D)].
    \mforall{}x:cat-ob(C).  ((functor-arrow(F)  x  x  (cat-id(C)  x))  =  (cat-id(D)  (functor-ob(F)  x)))


By

---

Latex:
(Auto  THEN  OnVar  `F'  DFunctor  THEN  Reduce  0  THEN  BackThruSomeHyp)

---

Home Index