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 β§ β y β     β‘β¨ ap! yβ‘yβ§z β©β‘
x β§ (y β§ z)   β‘β¨ associative semi β©β‘
β x β§ y β β§ z β‘Λβ¨ apΒ‘ xβ‘xβ§y β©β‘Λ
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 β§ 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 β§ 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 =
β y β β¨ z     β‘β¨ ap! y=xβ¨y β©β‘
(x β¨ y) β¨ z   β‘β¨ sym (associative semi) β©β‘
x β¨ β y β¨ z β β‘Λβ¨ apΒ‘ z=yβ¨z β©β‘Λ
x β¨ z         β

antisym : β {x y} β _ β _ β _
antisym {x} {y} y=xβ¨y 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 =
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) β