順序集合で圏(5)

ここらへんの続き。
dcpo (directed complete partial ordered set)*1 の定義。

順序集合 D が dcpo

D が有向余完備*2でかつ、始対象を持つ。

有向集合の定義は順序集合で圏(1)を参照。ここであれば単にフィルター圏であること。
文献によっては始対象の存在は要求しないこともあるらしい。

*1:単に cpo とも。

*2:有向な図式が常に余極限を持つこと。