open import Cat.Prelude

open import Order.Diagram.Glb
open import Order.Semilattice
open import Order.Base

import Order.Reasoning

module Order.Semilattice.Order where


# Semilattices from posetsπ

We have already established that semilattices, which we define algebraically, have an underlying poset. The aim of this module is to prove the converse: If you have a poset $(A, \le)$ such that any finite number of elements has a greatest lower bound, then $A$ is a semilattice. As usual, by induction, it suffices to have nullary and binary greatest lower bounds: A top element, and meets.

To this end, we define a type of finitely complete posets: Posets possessing meets and a top element.

record Finitely-complete-poset ββ βα΅£ : Type (lsuc (ββ β βα΅£)) where
no-eta-equality
field
poset : Poset ββ βα΅£
_β©_         : β poset β β β poset β β β poset β
has-is-meet : β {x y} β is-meet poset x y (x β© y)

top        : β poset β
has-is-top : β {x} β Poset._β€_ poset x top

open Poset poset public
private module meet {x} {y} = is-meet (has-is-meet {x} {y})

leβmeet : β {x y} β x β€ y β x β‘ x β© y
leβmeet xβ€y = le-meet poset xβ€y has-is-meet

meetβle : β {x y} β x β‘ x β© y β x β€ y


From a finitely complete poset, we can define a semilattice: from the universal property of meets, we can conclude that they are associative, idempotent, commutative, and have the top element as a unit.

fc-posetβsemilattice : β {o β} (P : Finitely-complete-poset o β) β Semilattice o
fc-posetβsemilattice P = to-semilattice make-p where
module ml = make-semilattice
open Finitely-complete-poset P

make-p : make-semilattice β poset β
make-p .ml.has-is-set = hlevel!
make-p .ml.top = top
make-p .ml.associative = β€-antisym

_ = le-meet