---

Step * of Lemma equal-functors

No Annotations
∀[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.  ((F x y f) = (G x y f) ∈ (cat-arrow(B) (F x) (F y)))) and 
     (∀x:cat-ob(A). ((F x) = (G x) ∈ cat-ob(B))))
BY
{ TACTIC:(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:
No  Annotations
\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.    ((F  x  y  f)  =  (G  x  y  f)))  and 
          (\mforall{}x:cat-ob(A).  ((F  x)  =  (G  x))))


By

---

Latex:
TACTIC:(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