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


  open Order.Reasoning P
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

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
Q.β€-antisym

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 =
f # m                Q.β€β

pres-tops
: β {t}
β is-top P t
β is-top Q (f # t)
pres-tops {t = t} t-top x =
f # Pβ.top Q.β€β¨ f .pres-β€ (t-top Pβ.top) β©Q.β€
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} {β}