Homotopy Type Theory join-semilattice > history (Rev #1)



A join-semilattice or finitely cocomplete (0,1)-category is a poset or (0,1)-category (P,)(P, \leq) with

  • a term :P\bot:P

  • a family of dependent terms

    a:Pt(a):aa:P \vdash t(a):\bot \leq a

    representing that \bot is initial in the poset.

  • a binary operation ()():P×PP(-)\vee(-):P \times P \to P

  • two families of dependent terms

    a:P,b:Pi a(a,b):aaba:P, b:P \vdash i_a(a, b):a \leq a \vee b
    a:P,b:Pi b(a,b):baba:P, b:P \vdash i_b(a, b):b \leq a \vee b
  • a family of dependent terms

    a:P,b:P,()():P×PP,i a(a,b):aab,i b(a,b):babi(a,b):(ab)(ab)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 10, 2022 at 18:50:26 by Anonymous?. See the history of this page for a list of all contributions to it.