---

Step * of Lemma equal-functors

∀[A,B:SmallCategory]. ∀[F,G:Functor(A;B)].
  (F = G ∈ Functor(A;B)) supposing 
     ((∀x,y:cat-ob(A). ∀f:cat-arrow(A) x y.
         ((arrow(F) x y f) = (arrow(G) x y f) ∈ (cat-arrow(B) (ob(F) x) (ob(F) y)))) and 
     (∀x:cat-ob(A). ((ob(F) x) = (ob(G) x) ∈ cat-ob(B))))
BY
{ (Auto
   THEN OnVar `F' DFunctor⋅
   THEN OnVar `G' DFunctor⋅
   THEN All Reduce
   THEN EqTypeCD
   THEN Reduce 0
   THEN Auto
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:SmallCategory].  \mforall{}[F,G:Functor(A;B)].
    (F  =  G)  supposing 
          ((\mforall{}x,y:cat-ob(A).  \mforall{}f:cat-arrow(A)  x  y.    ((arrow(F)  x  y  f)  =  (arrow(G)  x  y  f)))  and 
          (\mforall{}x:cat-ob(A).  ((ob(F)  x)  =  (ob(G)  x))))


By

---

Latex:
(Auto
  THEN  OnVar  `F'  DFunctor\mcdot{}
  THEN  OnVar  `G'  DFunctor\mcdot{}
  THEN  All  Reduce
  THEN  EqTypeCD
  THEN  Reduce  0
  THEN  Auto
  THEN  EqCD
  THEN  Auto)

---

Home Index