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

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
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 =
ub
(f # x) Qβ.β© (f # y) Q.β€
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β.top     Q.β€
f # Pβ.top Q.β€
f # t      Q.β€β

open is-meet-slat-hom

abstract
is-meet-slat-hom-is-prop
: β {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)

instance
H-Level-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π

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} {β}