---

Step * of Lemma mk-functor_wf

∀[A,B:SmallCategory]. ∀[F:cat-ob(A) ⟶ cat-ob(B)]. ∀[M:x:cat-ob(A)
                                                       ⟶ y:cat-ob(A)
                                                       ⟶ (cat-arrow(A) x y)
                                                       ⟶ (cat-arrow(B) F[x] F[y])].
  (functor(ob(a) = F[a];
           arrow(x,y,f) = M[x;y;f]) ∈ Functor(A;B)) supposing 
     ((∀x:cat-ob(A). (M[x;x;cat-id(A) x] = (cat-id(B) (F x)) ∈ (cat-arrow(B) (F x) (F x)))) and 
     (∀x,y,z:cat-ob(A). ∀f:cat-arrow(A) x y. ∀g:cat-arrow(A) y z.
        (M[x;z;cat-comp(A) x y z f g]
        = (cat-comp(B) (F x) (F y) (F z) M[x;y;f] M[y;z;g])
        ∈ (cat-arrow(B) (F x) (F z)))))
BY
{ (Auto THEN MemTypeCD THEN Auto THEN RepUR ``mk-functor`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:SmallCategory].  \mforall{}[F:cat-ob(A)  {}\mrightarrow{}  cat-ob(B)].  \mforall{}[M:x:cat-ob(A)
                                                                                                              {}\mrightarrow{}  y:cat-ob(A)
                                                                                                              {}\mrightarrow{}  (cat-arrow(A)  x  y)
                                                                                                              {}\mrightarrow{}  (cat-arrow(B)  F[x]  F[y])].
    (functor(ob(a)  =  F[a];
                      arrow(x,y,f)  =  M[x;y;f])  \mmember{}  Functor(A;B))  supposing 
          ((\mforall{}x:cat-ob(A).  (M[x;x;cat-id(A)  x]  =  (cat-id(B)  (F  x))))  and 
          (\mforall{}x,y,z:cat-ob(A).  \mforall{}f:cat-arrow(A)  x  y.  \mforall{}g:cat-arrow(A)  y  z.
                (M[x;z;cat-comp(A)  x  y  z  f  g]  =  (cat-comp(B)  (F  x)  (F  y)  (F  z)  M[x;y;f]  M[y;z;g]))))


By

---

Latex:
(Auto  THEN  MemTypeCD  THEN  Auto  THEN  RepUR  ``mk-functor``  0  THEN  Auto)

---

Home Index