# Homotopy Type Theory join-semilattice > history (changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

# Contents

## 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.