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 :
mk-cat: mk-cat,
equal: s = t ∈ T,
it: ⋅
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:
2020_05_20-AM-07_49_45
Last ObjectModification:
2017_01_13-PM-00_09_21
Theory : small!categories
Home
Index