Showing changes from revision #1 to #2:
Added | Removed | Changed
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
representing that $\top$ is terminal in the poset.
a binary operation $(-)\wedge(-):P \times P \to P$
two families of dependent terms
a family of dependent terms
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