---

Step * of Lemma arrow_mk_functor_lemma

∀g,y,x,arrow,ob:Top.  (arrow(functor(ob(a) = ob[a];arrow(u,v,f) = arrow[u;v;f])) x y g ~ arrow[x;y;g])
BY
{ (RepUR ``mk-functor functor-arrow`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g,y,x,arrow,ob:Top.
    (arrow(functor(ob(a)  =  ob[a];arrow(u,v,f)  =  arrow[u;v;f]))  x  y  g  \msim{}  arrow[x;y;g])


By

---

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

---

Home Index