Homotopy Type Theory
joinsemilattice > history (Rev #2)
Contents
Definition
A joinsemilattice 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
$a:P \vdash t(a):\bot \leq a$
representing that $\bot$ is initial in the poset.

a binary operation $()\vee():P \times P \to P$

two families of dependent terms
$a:P, b:P \vdash i_a(a, b):a \leq a \vee b$
$a:P, b:P \vdash i_b(a, b):b \leq a \vee b$

a family of dependent terms
$a:P, b:P, ()\oplus():P \times P \to P, i_a(a, b):a \leq a \oplus b, i_b(a, b):b \leq a \oplus b \vdash i(a,b):(a \vee b) \leq (a \oplus b)$
representing that $\vee$ is a coproduct in the poset.
See also
Revision on March 12, 2022 at 00:06:34 by
Anonymous?.
See the history of this page for a list of all contributions to it.