Homotopy Type Theory meet-semilattice > history (Rev #2)

Contents

Definition

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

  • a term :P\top:P

  • a family of dependent terms

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

    representing that \top is terminal in the poset.

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

  • two families of dependent terms

    a:P,b:Pp a(a,b):abaa:P, b:P \vdash p_a(a, b):a \wedge b \leq a
    a:P,b:Pp b(a,b):abba:P, b:P \vdash p_b(a, b):a \wedge b \leq b
  • a family of dependent terms

    a:P,b:P,()():P×PP,p a(a,b):aab,p b(a,b):babp(a,b):(ab)(ab)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 PP is only a (0,1)-precategory, then it is called a finitely complete (0,1)-precategory

See also

Revision on May 2, 2022 at 18:13:27 by Anonymous?. See the history of this page for a list of all contributions to it.