Nuprl Definition : mk-functor

functor(ob(a) = ob[a];
        arrow(x,y,f) = arrow[x;
                             y;
                             f]) ==
  <λa.ob[a]
  , λx,y,f. arrow[x;
                  y;
                  f]
  >


Definitions occuring in Statement :  lambda: λx.A[x],  pair: <a, b>
Definitions occuring in definition :  pair: <a, b>,  lambda: λx.A[x]
FDL editor aliases :  mk-functor
Latex:
functor(ob(a)  =  ob[a];
                arrow(x,y,f)  =  arrow[x;
                                                          y;
                                                          f])  ==
    <\mlambda{}a.ob[a]
    ,  \mlambda{}x,y,f.  arrow[x;
                                    y;
                                    f]
    >


Date html generated: 2020_05_20-AM-07_50_45
Last ObjectModification: 2017_01_13-PM-00_28_23

Theory : small!categories


Home Index