---

Step * of Lemma functor-arrow-id

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

---

Latex:

---

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


By

---

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

---

Home Index