Homotopy Type Theory
meetsemilattice > history (Rev #2)
Contents
Definition
A meetsemilattice 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
See also
Revision on May 2, 2022 at 14:13:27 by
Anonymous?.
See the history of this page for a list of all contributions to it.