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
    _∩_     : ⌞ 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.

    {P : Poset o β„“} {Q : Poset o' β„“'} (f : Monotone P Q)
    (P-slat : is-meet-semilattice P) (Q-slat : is-meet-semilattice Q)
    : Type (o βŠ” β„“')
    ∩-≀   : βˆ€ x y β†’ (f # x) Qβ‚—.∩ (f # y) Q.≀ f # (x Pβ‚—.∩ y)
    top-≀ : Qβ‚—.top Q.≀ f # Pβ‚—.top
  pres-∩ : βˆ€ x y β†’ f # (x Pβ‚—.∩ y) ≑ f # x Qβ‚—.∩ f # y
  pres-∩ x y =
      (Qβ‚—.∩-universal (f # (x Pβ‚—.∩ y))
        (f .pres-≀ Pβ‚—.βˆ©β‰€l)
        (f .pres-≀ Pβ‚—.βˆ©β‰€r))
      (∩-≀ x y)

  pres-top : f # Pβ‚—.top ≑ Qβ‚—.top
  pres-top = Q.≀-antisym Qβ‚—.! top-≀

    : βˆ€ {x y m}
    β†’ is-meet P x y m
    β†’ is-meet Q (f # x) (f # y) (f # m)
  pres-meets meet≀l = f .pres-≀ (meet .meet≀l)
  pres-meets meet≀r = f .pres-≀ (meet .meet≀r)
  pres-meets {x = x} {y = y} {m = m} meet .is-meet.greatest ub ub≀fx ub≀fy =
    ub                   Q.β‰€βŸ¨ Qβ‚—.∩-universal ub ub≀fx ub≀fy ⟩Q.≀
    (f # x) Qβ‚—.∩ (f # y) Q.β‰€βŸ¨ ∩-≀ x y ⟩Q.≀
    f # (x Pβ‚—.∩ y)       Q.β‰€βŸ¨ f .pres-≀ (meet .greatest (x Pβ‚—.∩ y) Pβ‚—.βˆ©β‰€l Pβ‚—.βˆ©β‰€r) ⟩Q.≀
    f # m                Q.β‰€βˆŽ

    : βˆ€ {t}
    β†’ is-top P t
    β†’ is-top Q (f # t)
  pres-tops {t = t} t-top x =
    x          Q.β‰€βŸ¨ Qβ‚—.! ⟩Q.≀
    Qβ‚—.top     Q.β‰€βŸ¨ top-≀ ⟩Q.≀
    f # Pβ‚—.top Q.β‰€βŸ¨ f .pres-≀ (t-top Pβ‚—.top) ⟩Q.≀
    f # t      Q.β‰€βˆŽ

open is-meet-slat-hom

    : βˆ€ {P : Poset o β„“} {Q : Poset o' β„“'} {f : Monotone P Q}
        {P-slat Q-slat}
    β†’ is-prop (is-meet-slat-hom f P-slat Q-slat)
  is-meet-slat-hom-is-prop =
    Iso→is-hlevel 1 eqv hlevel!
    where unquoteDecl eqv = declare-record-iso eqv (quote is-meet-slat-hom)

    : βˆ€ {f : Monotone P Q} {P-slat Q-slat n}
    β†’ H-Level (is-meet-slat-hom f P-slat Q-slat) (suc n)
  H-Level-is-meet-slat-hom = prop-instance is-meet-slat-hom-is-prop

The category of meet-semilatticesπŸ”—

  : βˆ€ (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

  : βˆ€ {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 β„“ = is-meet-semilattice
Meet-slats-subcat o β„“ = is-meet-slat-hom
Meet-slats-subcat o β„“ = hlevel!
Meet-slats-subcat o β„“ = id-meet-slat-hom
Meet-slats-subcat o β„“∘ = ∘-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} {β„“}