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 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 and

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 1
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} {β„“}