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