open import 1Lab.Prelude

open import Algebra.Semigroup

open import Cat.Diagram.Coproduct
open import Cat.Diagram.Product
open import Cat.Prelude
open import Cat.Thin

module Algebra.Semilattice where


# Semilattices🔗

A semilattice is a partially ordered set where all elements have a meet (a meet semilattice), or a join (a join semilattice). Rather than use a definition in terms of ordered sets, we choose an algebraic definition of semilattices: A semilattice $(A, \land)$ is a commutative semigroup where every element is idempotent: $x \land x = x$.

record is-semilattice (_∧_ : A → A → A) : Type (level-of A) where
field
has-is-semigroup : is-semigroup _∧_
commutative    : ∀ {x y} → x ∧ y ≡ y ∧ x
idempotent     : ∀ {x} → x ∧ x ≡ x

open is-semigroup has-is-semigroup public


## Order-theoretically🔗

Each semilattice structure $(A, \land)$ on $A$ induces two partial orders on $A$ by setting $x \le y$ when $x = x \land y$ or when $y = x \land y$. In the former case, we call the semilattice structure a meet semilattice, since the binary operation acts as a meet of $x$ and $y$, and similarly the dual choice is called a join semilattice. We detail the construction of a meet semilattice, and leave the construction of a join semilattice in a <details> tag.

Semilattice-on→Meet-on
: ∀ {∧ : A → A → A}
→ is-semilattice ∧
→ Poset (level-of A) (level-of A)
Semilattice-on→Meet-on {A = A} {∧ = _∧_} semi = r where
open Poset
open is-semilattice

rel : A → A → _
rel x y = (x ≡ x ∧ y)


As mentioned, the order relation is defined by setting $(x \le y) \leftrightarrow (x ≡ x ∧ y)$. For this to be reflexive, we need that $x ≡ (x ∧ x)$, which is guaranteed by the idempotence axiom:

  rel-refl : ∀ {x} → rel x x
rel-refl = sym (idempotent semi)


The relation is transitive by a use of associativity, as can be seen in the equational computation below:

  rel-transitive : ∀ {x y z} → rel x y → rel y z → rel x z
rel-transitive {x} {y} {z} x≡x∧y y≡y∧z =
x             ≡⟨ x≡x∧y ⟩≡
(x ∧ y)       ≡⟨ ap₂ _∧_ refl y≡y∧z ⟩≡
(x ∧ (y ∧ z)) ≡⟨ associative semi ⟩≡
((x ∧ y) ∧ z) ≡⟨ ap₂ _∧_ (sym x≡x∧y) refl ⟩≡
x ∧ z         ∎


The relation is propositional since it is equality in a set — the type $A$ is assumed to be a set since $(A, \land)$ must be a semigroup, and semigroups must be sets.

  rel-prop : ∀ {x y} → is-prop (rel x y)
rel-prop = has-is-set semi _ _


The relation is antisymmetric by a use of commutativitiy:

  rel-antisym : ∀ {x y} → rel x y → rel y x → x ≡ y
rel-antisym {x} {y} x≡x∧y y≡y∧x =
x     ≡⟨ x≡x∧y ⟩≡
x ∧ y ≡⟨ commutative semi ⟩≡
y ∧ x ≡⟨ sym y≡y∧x ⟩≡
y     ∎


This data defines a poset:

  r = make-poset {R = rel} rel-refl rel-transitive rel-antisym rel-prop


We now prove that, under this relation, $x \land y$ is the product of $x$ and $y$. Since the product of two objects $x$, $y$ in a thin category is the largest object which is still smaller than $x$ and $y$, we refer to it as a meet, to keep with the order-theoretic naming. First, we must show that $x \land y$ admits “maps into” (i.e., is lesser than or equal to) $x$ and $y$.

module _ {_∧_ : A → A → A} (semi : is-semilattice _∧_) where
private Po = Semilattice-on→Meet-on semi
open Poset Po
open is-semilattice semi

∧-less-thanl : ∀ {x y} → (x ∧ y) ≤ x
∧-less-thanl {x} {y} = sym (
(x ∧ y) ∧ x ≡⟨ commutative ⟩≡
x ∧ (x ∧ y) ≡⟨ associative semi ⟩≡
(x ∧ x) ∧ y ≡⟨ ap (_∧ _) idempotent ⟩≡
x ∧ y       ∎)

∧-less-thanr : ∀ {x y} → (x ∧ y) ≤ y
∧-less-thanr {x} {y} =
x ∧ y       ≡˘⟨ ap (_ ∧_) idempotent ⟩≡˘
x ∧ (y ∧ y) ≡⟨ associative semi ⟩≡
(x ∧ y) ∧ y ∎


We can now prove that this cone is universal. Since the less-than relation in a poset is a proposition, the only thing that must be shown is that if $q \le x$ and $q \le y$, then $q \le (x \land y)$.

  Semilattice→is-product
: ∀ {x y} → is-product underlying {P = x ∧ y} ∧-less-thanl ∧-less-thanr
Semilattice→is-product {x} {y} = r where
open is-product

r : is-product _ _ _
r .π₁∘factor = Hom-is-prop _ _ _ _
r .π₂∘factor = Hom-is-prop _ _ _ _
r .unique _ _ _ = Hom-is-prop _ _ _ _


Fortunately, a neat little calculation is all we need:

    r .⟨_,_⟩ {Q} q=q∧x q=q∧y =
Q           ≡⟨ q=q∧y ⟩≡
Q ∧ y       ≡⟨ ap (_∧ _) q=q∧x ⟩≡
(Q ∧ x) ∧ y ≡˘⟨ associative semi ⟩≡˘
Q ∧ (x ∧ y) ∎

The construction of a join semilattice is formally dual, and so we leave it in this details tag in the interest of conciseness.
Semilattice-on→Join-on
: ∀ {∨ : A → A → A} → is-semilattice ∨ → Poset (level-of A) (level-of A)
Semilattice-on→Join-on {∨ = _∨_} semi = r where
open is-semilattice

transitive : ∀ {x y z} → y ≡ x ∨ y → z ≡ y ∨ z → _
transitive {x} {y} {z} y=x∨y z=y∨z =
z           ≡⟨ z=y∨z ⟩≡
y ∨ z       ≡⟨ ap₂ _∨_ y=x∨y refl ⟩≡
(x ∨ y) ∨ z ≡⟨ sym (associative semi) ⟩≡
x ∨ (y ∨ z) ≡⟨ ap₂ _∨_ refl (sym z=y∨z) ⟩≡
x ∨ z ∎

antisym : ∀ {x y} → _ → _ → _
antisym {x} {y} y=x∨y x=y∨x =
x     ≡⟨ x=y∨x ⟩≡
y ∨ x ≡⟨ commutative semi ⟩≡
x ∨ y ≡⟨ sym y=x∨y ⟩≡
y     ∎

r : Poset _ _
r = make-poset
{R = λ x y → y ≡ (x ∨ y)}
(sym (idempotent semi)) transitive antisym (has-is-set semi _ _)


We also have that, under this order relation, the semilattice operator gives the coproduct (join) of the operands, as promised.

module _ {_∨_ : A → A → A} (semi : is-semilattice _∨_) where
private Po = Semilattice-on→Join-on semi
open Poset Po
open is-semilattice semi

∨-greater-thanl : ∀ {x y} → x ≤ (x ∨ y)
∨-greater-thanl {x} {y} =
x ∨ y       ≡˘⟨ ap (_∨ _) idempotent ⟩≡˘
(x ∨ x) ∨ y ≡˘⟨ associative semi ⟩≡˘
x ∨ (x ∨ y) ∎

∨-greater-thanr : ∀ {x y} → y ≤ (x ∨ y)
∨-greater-thanr {x} {y} =
x ∨ y       ≡˘⟨ ap (_ ∨_) idempotent ⟩≡˘
x ∨ (y ∨ y) ≡⟨ associative semi ⟩≡
(x ∨ y) ∨ y ≡˘⟨ ap (_∨ _) commutative ⟩≡˘
(y ∨ x) ∨ y ≡˘⟨ associative semi ⟩≡˘
y ∨ (x ∨ y) ∎

Semilattice→is-coproduct
: ∀ {x y} → is-coproduct underlying {P = x ∨ y} ∨-greater-thanl ∨-greater-thanr
Semilattice→is-coproduct {x} {y} = c where
open is-coproduct
c : is-coproduct _ _ _
c .[_,_] {Q} q=x∨q q=y∨q =
Q           ≡⟨ q=x∨q ⟩≡
x ∨ Q       ≡⟨ ap (_ ∨_) q=y∨q ⟩≡
x ∨ (y ∨ Q) ≡⟨ associative semi ⟩≡
(x ∨ y) ∨ Q ∎
c .in₀∘factor = Hom-is-prop _ _ _ _
c .in₁∘factor = Hom-is-prop _ _ _ _
c .unique _ _ _ = Hom-is-prop _ _ _ _


## Maps🔗

As is typical with algebraic structures, we define a semilattice homomorphism as being a map which commutes with the binary operator. Since being a semilattice is a property of $(A, \land)$, we have a characterisation of identifications of semilattices: Two semilattices are identified precisely when their underlying types are equivalent by some homomorphic equivalence.

private unquoteDecl eqv = declare-record-iso eqv (quote is-semilattice)

instance
H-Level-is-semilattice : ∀ {M : A → A → A} {n} → H-Level (is-semilattice M) (suc n)
H-Level-is-semilattice = prop-instance λ x →
let open is-semilattice x in is-hlevel≃ 1 (Iso→Equiv eqv e⁻¹) (hlevel 1) x


A semilattice structure on a type $A$ equips the type with an operator $\land$ and the proof that this operator has the properties of a semilattice.

record Semilattice-on {ℓ} (A : Type ℓ) : Type ℓ where
field
∧ : A → A → A
has-is-semilattice : is-semilattice ∧

open is-semilattice has-is-semilattice public

-- Considered as a meet-semilattice:
→Meet : Poset ℓ ℓ
→Meet = Semilattice-on→Meet-on has-is-semilattice

-- Considered as a join-semilattice:
→Join : Poset ℓ ℓ
→Join = Semilattice-on→Join-on has-is-semilattice

∨ : A → A → A
∨ = ∧

open Semilattice-on using (→Meet ; →Join)

Semilattice : ∀ ℓ → Type (lsuc ℓ)
Semilattice ℓ = Σ (Semilattice-on {ℓ = ℓ})


The property is-semilattice-hom follows the trend of naming the operator $\land$; However, it also exports a renaming of the preservation datum pres-∧ which refers to the operator as $\lor$.

record is-semilattice-hom (A B : Semilattice ℓ) (f : A .fst → B .fst) : Type ℓ where
private
module A = Semilattice-on (A .snd)
module B = Semilattice-on (B .snd)

field
pres-∧ : ∀ x y → f (A.∧ x y) ≡ B.∧ (f x) (f y)

-- Considered as a homomorphism of join semilattices:

pres-∨ : ∀ x y → f (A.∨ x y) ≡ B.∨ (f x) (f y)
pres-∨ = pres-∧

Semilattice≃ : (A B : Semilattice ℓ) (f : A .fst ≃ B .fst) → Type ℓ
Semilattice≃ A B = is-semilattice-hom A B ∘ fst


Using the automated machinery for deriving is-univalent proofs, we get the promised characterisation of identifications in the type of semilattices.

Semilattice-univalent : ∀ {ℓ} → is-univalent (HomT→Str (Semilattice≃ {ℓ = ℓ}))
Semilattice-univalent {ℓ = ℓ} =
Derive-univalent-record (record-desc (Semilattice-on {ℓ = ℓ}) Semilattice≃
(record:
field[ Semilattice-on.∧ by is-semilattice-hom.pres-∧ ]
axiom[ Semilattice-on.has-is-semilattice by (λ _ → hlevel 1) ]))


Any semilattice homomorphism is monotone when considered as a map between the posets induced by a semilattice, regardless of whether we consider it as a meet or as a join semilattice.

module _
{A B : Semilattice ℓ} (f : A .fst → B .fst) (ishom : is-semilattice-hom A B f)
where
private
module A = Semilattice-on (A .snd)
module B = Semilattice-on (B .snd)

open is-semilattice-hom ishom

is-semilattice-hom→is-monotone-meet
: Monotone-map A.→Meet B.→Meet
is-semilattice-hom→is-monotone-meet =
make-monotone-map A.→Meet B.→Meet f λ x y x=x∧y →
f x             ≡⟨ ap f x=x∧y ⟩≡
f (A.∧ x y)     ≡⟨ pres-∧ _ _ ⟩≡
B.∧ (f x) (f y) ∎

is-semilattice-hom→is-monotone-join
: Monotone-map A.→Join B.→Join
is-semilattice-hom→is-monotone-join =
make-monotone-map A.→Join B.→Join f λ x y y=x∨y →
f y             ≡⟨ ap f y=x∨y ⟩≡
f (A.∨ x y)     ≡⟨ pres-∨ _ _ ⟩≡
B.∨ (f x) (f y) ∎