module Order.Semilattice.Meet where

Meet semilatticesπŸ”—

A meet semilattice is a partially ordered set which has all finite meets. This means, in particular, that it has a top element, since that is the meet of the empty family. Note that, even though meet-semilattices are presented as being equipped with a binary operation a∩ba \cap b, this is not actual structure on the partially-ordered set: meets are uniquely determined, so β€œbeing a meet-semilattice” is always a proposition.

record is-meet-semilattice {o β„“} (P : Poset o β„“) : Type (o βŠ” β„“) where
  field
    _∩_     : ⌞ P ⌟ β†’ ⌞ P ⌟ β†’ ⌞ P ⌟
    ∩-meets : βˆ€ x y β†’ is-meet P x y (x ∩ y)
    has-top : Top P

  infixr 25 _∩_

A homomorphism of meet-semilattices is a monotone function that sends finite meets to finite meets. In particular, it suffices to have βŠ€β‰€f(⊀)\top \le f(\top), and

f(a)∩f(b)≀f(a∩b), f(a) \cap f(b) \le f(a \cap b)\text{,}

since the converse direction of these inequalities is guaranteed by the universal properties.

record
  is-meet-slat-hom
    {P : Poset o β„“} {Q : Poset o' β„“'} (f : Monotone P Q)
    (P-slat : is-meet-semilattice P) (Q-slat : is-meet-semilattice Q)
    : Type (o βŠ” β„“')
  where
  field
    ∩-≀   : βˆ€ x y β†’ (f # x) Qβ‚—.∩ (f # y) Q.≀ f # (x Pβ‚—.∩ y)
    top-≀ : Qβ‚—.top Q.≀ f # Pβ‚—.top

The category of meet-semilatticesπŸ”—

id-meet-slat-hom
  : βˆ€ (Pβ‚— : is-meet-semilattice P)
  β†’ is-meet-slat-hom idβ‚˜ Pβ‚— Pβ‚—
id-meet-slat-hom {P = P} _ .∩-≀ _ _ = Poset.≀-refl P
id-meet-slat-hom {P = P} _ .top-≀ = Poset.≀-refl P

∘-meet-slat-hom
  : βˆ€ {Pβ‚— Qβ‚— Rβ‚—} {f : Monotone Q R} {g : Monotone P Q}
  β†’ is-meet-slat-hom f Qβ‚— Rβ‚—
  β†’ is-meet-slat-hom g Pβ‚— Qβ‚—
  β†’ is-meet-slat-hom (f βˆ˜β‚˜ g) Pβ‚— Rβ‚—
∘-meet-slat-hom {R = R} {f = f} {g = g} f-pres g-pres .∩-≀ x y =
  R .Poset.≀-trans (f-pres .∩-≀ (g # x) (g # y)) (f .pres-≀ (g-pres .∩-≀ x y))
∘-meet-slat-hom {R = R} {f = f} {g = g} f-pres g-pres .top-≀ =
  R .Poset.≀-trans (f-pres .top-≀) (f .pres-≀ (g-pres .top-≀))
Meet-slats-subcat : βˆ€ o β„“ β†’ Subcat (Posets o β„“) (o βŠ” β„“) (o βŠ” β„“)
Meet-slats-subcat o β„“ .Subcat.is-ob = is-meet-semilattice
Meet-slats-subcat o β„“ .Subcat.is-hom = is-meet-slat-hom
Meet-slats-subcat o β„“ .Subcat.is-hom-prop = hlevel!
Meet-slats-subcat o β„“ .Subcat.is-hom-id = id-meet-slat-hom
Meet-slats-subcat o β„“ .Subcat.is-hom-∘ = ∘-meet-slat-hom

Meet-slats : βˆ€ o β„“ β†’ Precategory (lsuc o βŠ” lsuc β„“) (o βŠ” β„“)
Meet-slats o β„“ = Subcategory (Meet-slats-subcat o β„“)
module Meet-slats {o} {β„“} = Cat.Reasoning (Meet-slats o β„“)

Meet-semilattice : βˆ€ o β„“ β†’ Type _
Meet-semilattice o β„“ = Meet-slats.Ob {o} {β„“}