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