open import Cat.Functor.Subcategory
open import Cat.Prelude

open import Data.Fin.Base hiding (_≀_)

open import Order.Diagram.Meet
open import Order.Diagram.Glb
open import Order.Diagram.Top
open import Order.Base

import Cat.Reasoning

import Order.Diagram.Meet.Reasoning as Meets
import Order.Reasoning
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 _∩_
  open Order.Reasoning P
  open Meets ∩-meets public
  open Top has-top using (top; !) public

abstract
  is-meet-semilattice-is-prop
    : βˆ€ {o β„“} {P : Poset o β„“}
    β†’ is-prop (is-meet-semilattice P)
  is-meet-semilattice-is-prop {P = P} p q = path where
    open Order.Diagram.Top P using (H-Level-Top)
    open is-meet-semilattice
    module p = is-meet-semilattice p
    module q = is-meet-semilattice q

    meetp : βˆ€ x y β†’ x p.∩ y ≑ x q.∩ y
    meetp x y = meet-unique (p.∩-meets x y) (q.∩-meets x y)

    path : p ≑ q
    path i ._∩_ x y     = meetp x y i
    path i .∩-meets x y = is-propβ†’pathp (Ξ» i β†’ hlevel {T = is-meet P x y (meetp x y i)} 1) (p.∩-meets x y) (q.∩-meets x y) i
    path i .has-top     = hlevel {T = Top P} 1 p.has-top q.has-top i

private variable
  o β„“ o' β„“' : Level
  P Q R : Poset o β„“

instance
  H-Level-is-meet-semilattice : βˆ€ {n} β†’ H-Level (is-meet-semilattice P) (suc n)
  H-Level-is-meet-semilattice = prop-instance is-meet-semilattice-is-prop

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
  no-eta-equality
  private
    module P = Poset P
    module Pβ‚— = is-meet-semilattice P-slat
    module Q = Order.Reasoning Q
    module Qβ‚— = is-meet-semilattice Q-slat
    open is-meet
  field
    ∩-≀   : βˆ€ 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.≀-antisym
      (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-≀

  pres-meets
    : βˆ€ {x y m}
    β†’ is-meet P x y m
    β†’ is-meet Q (f Β· x) (f Β· y) (f Β· m)
  pres-meets meet .is-meet.meet≀l = f .pres-≀ (meet .meet≀l)
  pres-meets meet .is-meet.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 ⟩
    (f Β· x) Qβ‚—.∩ (f Β· y) Q.β‰€βŸ¨ ∩-≀ x y ⟩
    f Β· (x Pβ‚—.∩ y)       Q.β‰€βŸ¨ f .pres-≀ (meet .greatest (x Pβ‚—.∩ y) Pβ‚—.βˆ©β‰€l Pβ‚—.βˆ©β‰€r) ⟩
    f Β· m                Q.β‰€βˆŽ

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

open is-meet-slat-hom

unquoteDecl H-Level-is-meet-slat-hom = declare-record-hlevel 1 H-Level-is-meet-slat-hom (quote is-meet-slat-hom)

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