[[!redirects finitely cocomplete (0,1)-precategory]] #Contents# * table of contents {:toc} ## Definition ## A __join-semilattice__ or __finitely cocomplete (0,1)-category__ is a [[poset]] or (0,1)-category $(P, \leq)$ with * a term $\bot:P$ * a family of dependent terms $$a:P \vdash t(a):\bot \leq a$$ representing that $\bot$ is initial in the poset. * a binary operation $(-)\vee(-):P \times P \to P$ * two families of dependent terms $$a:P, b:P \vdash i_a(a, b):a \leq a \vee b$$ $$a:P, b:P \vdash i_b(a, b):b \leq a \vee b$$ * a family of dependent terms $$a:P, b:P, (-)\oplus(-):P \times P \to P, i_a(a, b):a \leq a \oplus b, i_b(a, b):b \leq a \oplus b \vdash i(a,b):(a \vee b) \leq (a \oplus b)$$ representing that $\vee$ is a coproduct in the poset. ## See also ## * [[poset]] * [[meet-semilattice]] * [[lattice]] * [[omega-complete poset]]