Nuprl Definition : mk-cat

Cat(ob = ob;
    arrow(x,y) = arrow[x; y];
    id(a) = id[a];
    comp(u,v,w,f,g) = comp[u;
                           v;
                           w;
                           f;
                           g]) ==
  <ob
  , λx,y. arrow[x; y]
  , λa.id[a]
  , λu,v,w,f,g. comp[u;
                     v;
                     w;
                     f;
                     g]>

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-cat

Latex:
Cat(ob = ob; arrow(x,y) = arrow[x; y]; id(a) = id[a]; comp(u,v,w,f,g) = comp[u; v; w; f; g]) == <ob , \mlambda{}x,y. arrow[x; y] , \mlambda{}a.id[a] , \mlambda{}u,v,w,f,g. comp[u; v; w; f; g]> Date html generated: 2020_05_20-AM-07_49_41 Last ObjectModification: 2017_01_13-AM-11_00_55 Theory : small!categories Home Index