Nuprl Definition : discrete-cat
discrete-cat(X) ==  Cat(ob = X;arrow(x,y) = x = y ∈ X;id(a) = ⋅;comp(u,v,w,f,g) = ⋅)
Definitions occuring in Statement : 
mk-cat: mk-cat, 
it: ⋅
, 
equal: s = t ∈ T
Definitions occuring in definition : 
it: ⋅
, 
equal: s = t ∈ T
, 
mk-cat: mk-cat
FDL editor aliases : 
discrete-cat
Latex:
discrete-cat(X)  ==    Cat(ob  =  X;arrow(x,y)  =  x  =  y;id(a)  =  \mcdot{};comp(u,v,w,f,g)  =  \mcdot{})
Date html generated:
2017_01_19-PM-02_51_50
Last ObjectModification:
2017_01_13-PM-00_09_21
Theory : small!categories
Home
Index