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,∧)(A, \land) is a commutative semigroup where every element is idempotent: x∧x=xx \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,∧)(A, \land) on AA induces two partial orders on AA by setting x≀yx \le y when x=x∧yx = x \land y or when y=x∧yy = 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.

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≀y)↔(x≑x∧y)(x \le y) \leftrightarrow (x ≑ x ∧ y). For this to be reflexive, we need that x≑(x∧x)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! 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 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 βŸ©β‰‘
    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∧yx \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 x∧yx \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 q≀xq \le x and q≀yq \le y, then q≀(x∧y)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 βŸ©β‰‘
    (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 =
     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,∧)(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 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
  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) ∎