---

Step * of Lemma equal-functors1

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

---

Latex:

---

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


By

---

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

---

Home Index