Homotopy Type Theory meet-semilattice > history (changes)

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

Contents

Definition

A meet-semilattice or finitely complete (0,1)-category is a poset or (0,1)-category $(P, \leq)$ with

• a term $\top:P$

• a family of dependent terms

$a:P \vdash t(a):a \leq \top$

representing that $\top$ is terminal in the poset.

• a binary operation $(-)\wedge(-):P \times P \to P$

• two families of dependent terms

$a:P, b:P \vdash p_a(a, b):a \wedge b \leq a$
$a:P, b:P \vdash p_b(a, b):a \wedge b \leq b$
• a family of dependent terms

$a:P, b:P, (-)\otimes(-):P \times P \to P, p_a(a, b):a \leq a \otimes b, p_b(a, b):b \leq a \otimes b \vdash p(a,b):(a \otimes b) \leq (a \wedge b)$

representing that $\wedge$ is a product in the poset.

If $P$ is only a (0,1)-precategory, then it is called a finitely complete (0,1)-precategory