[[!redirects finitely complete (0,1)-precategory]] #Contents# * table of contents {:toc} ## 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__ ## See also ## * [[poset]] * [[join-semilattice]] * [[lattice]]