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 : lambda: λx.A[x], pair: <a, b>
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: 2017_01_19-PM-02_51_41 Last ObjectModification: 2017_01_13-AM-11_00_55 Theory : small!categories Home Index