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


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,)(A, \land) is a commutative semigroup where every element is idempotent: xx=xx \land x = x.

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

  open is-semigroup has-is-semigroup public


Each semilattice structure (A,)(A, \land) on AA induces two partial orders on AA by setting xyx \le y when x=xyx = x \land y or when y=xyy = x \land y. In the former case, we call the semilattice structure a meet semilattice, since the binary operation acts as a meet of xx and yy, 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.

  :  { : A  A  A}
   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 (xy)(xxy)(x \le y) \leftrightarrow (x ≡ x ∧ y). For this to be reflexive, we need that x(xx)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 AA is assumed to be a set since (A,)(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 

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, xyx \land y is the product of xx and yy. Since the product of two objects xx, yy in a thin category is the largest object which is still smaller than xx and yy, we refer to it as a meet, to keep with the order-theoretic naming. First, we must show that xyx \land y admits “maps into” (i.e., is lesser than or equal to) xx and yy.

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 qxq \le x and qyq \le y, then q(xy)q \le (x \land y).

    :  {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.
  :  { : 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 

  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) 

    :  {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 _ _ _ _


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,)(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)

  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 AA 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
     : 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
    module A = Semilattice-on (A .snd)
    module B = Semilattice-on (B .snd)

    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≃
      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)
      module A = Semilattice-on (A .snd)
      module B = Semilattice-on (B .snd)

    open is-semilattice-hom ishom

      : 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) 

      : 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)