---

Step * of Lemma arrow_mk_functor_lemma

No Annotations
∀g,y,x,arrow,ob:Top.  (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:
No  Annotations
\mforall{}g,y,x,arrow,ob:Top.    (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