Join-semilattices

module order-theory.join-semilattices where

open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.semigroups

open import order-theory.least-upper-bounds-posets
open import order-theory.posets
open import order-theory.preorders
open import order-theory.upper-bounds-posets

Idea

A join-semilattice is a poset in which every pair of elements has a least binary upper bound. Alternatively, join-semilattices can be defined algebraically as a set X equipped with a binary operation ∧ : X → X → X satisfying

1. Asociativity: (x ∧ y) ∧ z ＝ x ∧ (y ∧ z),
2. Commutativity: x ∧ y ＝ y ∧ x,
3. Idempotency: x ∧ x ＝ x.

Note that this definition is identical to the definition of meet-semilattices. We will follow the algebraic approach for our principal definition of join-semilattices, since it requires only one universe level. This is necessary in order to consider the large category of join-semilattices.

Definitions

The predicate on semigroups of being a join-semilattice

module _
  {l : Level} (X : Semigroup l)
  where

  is-join-semilattice-Semigroup-Prop : Prop l
  is-join-semilattice-Semigroup-Prop =
    prod-Prop
      ( Π-Prop
        ( type-Semigroup X)
        ( λ x →
          Π-Prop
            ( type-Semigroup X)
            ( λ y →
              Id-Prop
                ( set-Semigroup X)
                ( mul-Semigroup X x y)
                ( mul-Semigroup X y x))))
      ( Π-Prop
        ( type-Semigroup X)
        ( λ x →
          Id-Prop
            ( set-Semigroup X)
            ( mul-Semigroup X x x)
            ( x)))

  is-join-semilattice-Semigroup : UU l
  is-join-semilattice-Semigroup =
    type-Prop is-join-semilattice-Semigroup-Prop

  is-prop-is-join-semilattice-Semigroup :
    is-prop is-join-semilattice-Semigroup
  is-prop-is-join-semilattice-Semigroup =
    is-prop-type-Prop is-join-semilattice-Semigroup-Prop

The algebraic definition of join-semilattices

Join-Semilattice : (l : Level) → UU (lsuc l)
Join-Semilattice l = type-subtype is-join-semilattice-Semigroup-Prop

module _
  {l : Level} (X : Join-Semilattice l)
  where

  semigroup-Join-Semilattice : Semigroup l
  semigroup-Join-Semilattice = pr1 X

  set-Join-Semilattice : Set l
  set-Join-Semilattice = set-Semigroup semigroup-Join-Semilattice

  type-Join-Semilattice : UU l
  type-Join-Semilattice = type-Semigroup semigroup-Join-Semilattice

  is-set-type-Join-Semilattice : is-set type-Join-Semilattice
  is-set-type-Join-Semilattice =
    is-set-type-Semigroup semigroup-Join-Semilattice

  join-Join-Semilattice : (x y : type-Join-Semilattice) → type-Join-Semilattice
  join-Join-Semilattice = mul-Semigroup semigroup-Join-Semilattice

  join-Join-Semilattice' : (x y : type-Join-Semilattice) → type-Join-Semilattice
  join-Join-Semilattice' x y = join-Join-Semilattice y x

  private
    _∨_ = join-Join-Semilattice

  associative-join-Join-Semilattice :
    (x y z : type-Join-Semilattice) → ((x ∨ y) ∨ z) ＝ (x ∨ (y ∨ z))
  associative-join-Join-Semilattice =
    associative-mul-Semigroup semigroup-Join-Semilattice

  is-join-semilattice-Join-Semilattice :
    is-join-semilattice-Semigroup semigroup-Join-Semilattice
  is-join-semilattice-Join-Semilattice = pr2 X

  commutative-join-Join-Semilattice :
    (x y : type-Join-Semilattice) → (x ∨ y) ＝ (y ∨ x)
  commutative-join-Join-Semilattice =
    pr1 is-join-semilattice-Join-Semilattice

  idempotent-join-Join-Semilattice :
    (x : type-Join-Semilattice) → (x ∨ x) ＝ x
  idempotent-join-Join-Semilattice =
    pr2 is-join-semilattice-Join-Semilattice

  leq-Join-Semilattice-Prop :
    (x y : type-Join-Semilattice) → Prop l
  leq-Join-Semilattice-Prop x y =
    Id-Prop set-Join-Semilattice (x ∨ y) y

  leq-Join-Semilattice :
    (x y : type-Join-Semilattice) → UU l
  leq-Join-Semilattice x y = type-Prop (leq-Join-Semilattice-Prop x y)

  is-prop-leq-Join-Semilattice :
    (x y : type-Join-Semilattice) → is-prop (leq-Join-Semilattice x y)
  is-prop-leq-Join-Semilattice x y =
    is-prop-type-Prop (leq-Join-Semilattice-Prop x y)

  private
    _≤_ = leq-Join-Semilattice

  refl-leq-Join-Semilattice :
    (x : type-Join-Semilattice) → x ≤ x
  refl-leq-Join-Semilattice x = idempotent-join-Join-Semilattice x

  transitive-leq-Join-Semilattice :
    (x y z : type-Join-Semilattice) → y ≤ z → x ≤ y → x ≤ z
  transitive-leq-Join-Semilattice x y z H K =
    equational-reasoning
      x ∨ z
      ＝ x ∨ (y ∨ z)
        by ap (join-Join-Semilattice x) (inv H)
      ＝ (x ∨ y) ∨ z
        by inv (associative-join-Join-Semilattice x y z)
      ＝ y ∨ z
        by ap (join-Join-Semilattice' z) K
      ＝ z
        by H

  antisymmetric-leq-Join-Semilattice :
    (x y : type-Join-Semilattice) →
    leq-Join-Semilattice x y → leq-Join-Semilattice y x → x ＝ y
  antisymmetric-leq-Join-Semilattice x y H K =
    equational-reasoning
      x ＝ y ∨ x
          by inv K
        ＝ x ∨ y
          by commutative-join-Join-Semilattice y x
        ＝ y
          by H

  preorder-Join-Semilattice : Preorder l l
  pr1 preorder-Join-Semilattice = type-Join-Semilattice
  pr1 (pr2 preorder-Join-Semilattice) = leq-Join-Semilattice-Prop
  pr1 (pr2 (pr2 preorder-Join-Semilattice)) = refl-leq-Join-Semilattice
  pr2 (pr2 (pr2 preorder-Join-Semilattice)) = transitive-leq-Join-Semilattice

  poset-Join-Semilattice : Poset l l
  pr1 poset-Join-Semilattice = preorder-Join-Semilattice
  pr2 poset-Join-Semilattice = antisymmetric-leq-Join-Semilattice

  is-binary-upper-bound-join-Join-Semilattice :
    (x y : type-Join-Semilattice) →
    is-binary-upper-bound-Poset
      ( poset-Join-Semilattice)
      ( x)
      ( y)
      ( join-Join-Semilattice x y)
  pr1 (is-binary-upper-bound-join-Join-Semilattice x y) =
    equational-reasoning
      x ∨ (x ∨ y)
      ＝ (x ∨ x) ∨ y
        by
        inv (associative-join-Join-Semilattice x x y)
      ＝ x ∨ y
        by
        ap (join-Join-Semilattice' y) (idempotent-join-Join-Semilattice x)
  pr2 (is-binary-upper-bound-join-Join-Semilattice x y) =
    equational-reasoning
      y ∨ (x ∨ y)
      ＝ (x ∨ y) ∨ y
        by commutative-join-Join-Semilattice y (x ∨ y)
      ＝ x ∨ (y ∨ y)
        by
        associative-join-Join-Semilattice x y y
      ＝ x ∨ y
        by
        ap (join-Join-Semilattice x) (idempotent-join-Join-Semilattice y)

  is-least-binary-upper-bound-join-Join-Semilattice :
    (x y : type-Join-Semilattice) →
    is-least-binary-upper-bound-Poset
      ( poset-Join-Semilattice)
      ( x)
      ( y)
      ( join-Join-Semilattice x y)
  is-least-binary-upper-bound-join-Join-Semilattice x y =
    prove-is-least-binary-upper-bound-Poset
      ( poset-Join-Semilattice)
      ( is-binary-upper-bound-join-Join-Semilattice x y)
      ( λ z (H , K) →
        equational-reasoning
          (x ∨ y) ∨ z
          ＝ x ∨ (y ∨ z)
            by associative-join-Join-Semilattice x y z
          ＝ x ∨ z
            by ap (join-Join-Semilattice x) K
          ＝ z
            by H)

The predicate on posets of being a join-semilattice

module _
  {l1 l2 : Level} (P : Poset l1 l2)
  where

  is-join-semilattice-Poset-Prop : Prop (l1 ⊔ l2)
  is-join-semilattice-Poset-Prop =
    Π-Prop
      ( type-Poset P)
      ( λ x →
        Π-Prop
          ( type-Poset P)
          ( has-least-binary-upper-bound-Poset-Prop P x))

  is-join-semilattice-Poset : UU (l1 ⊔ l2)
  is-join-semilattice-Poset = type-Prop is-join-semilattice-Poset-Prop

  is-prop-is-join-semilattice-Poset :
    is-prop is-join-semilattice-Poset
  is-prop-is-join-semilattice-Poset =
    is-prop-type-Prop is-join-semilattice-Poset-Prop

  module _
    (H : is-join-semilattice-Poset)
    where

    join-is-join-semilattice-Poset :
      type-Poset P → type-Poset P → type-Poset P
    join-is-join-semilattice-Poset x y = pr1 (H x y)

    is-least-binary-upper-bound-join-is-join-semilattice-Poset :
      (x y : type-Poset P) →
      is-least-binary-upper-bound-Poset P x y
        ( join-is-join-semilattice-Poset x y)
    is-least-binary-upper-bound-join-is-join-semilattice-Poset x y =
      pr2 (H x y)

The order-theoretic definition of join semilattices

Order-Theoretic-Join-Semilattice : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Order-Theoretic-Join-Semilattice l1 l2 =
  Σ (Poset l1 l2) is-join-semilattice-Poset

module _
  {l1 l2 : Level} (A : Order-Theoretic-Join-Semilattice l1 l2)
  where

  poset-Order-Theoretic-Join-Semilattice : Poset l1 l2
  poset-Order-Theoretic-Join-Semilattice = pr1 A

  type-Order-Theoretic-Join-Semilattice : UU l1
  type-Order-Theoretic-Join-Semilattice =
    type-Poset poset-Order-Theoretic-Join-Semilattice

  is-set-type-Order-Theoretic-Join-Semilattice :
    is-set type-Order-Theoretic-Join-Semilattice
  is-set-type-Order-Theoretic-Join-Semilattice =
    is-set-type-Poset poset-Order-Theoretic-Join-Semilattice

  set-Order-Theoretic-Join-Semilattice : Set l1
  set-Order-Theoretic-Join-Semilattice =
    set-Poset poset-Order-Theoretic-Join-Semilattice

  leq-Order-Theoretic-Join-Semilattice-Prop :
    (x y : type-Order-Theoretic-Join-Semilattice) → Prop l2
  leq-Order-Theoretic-Join-Semilattice-Prop =
    leq-Poset-Prop poset-Order-Theoretic-Join-Semilattice

  leq-Order-Theoretic-Join-Semilattice :
    (x y : type-Order-Theoretic-Join-Semilattice) → UU l2
  leq-Order-Theoretic-Join-Semilattice =
    leq-Poset poset-Order-Theoretic-Join-Semilattice

  is-prop-leq-Order-Theoretic-Join-Semilattice :
    (x y : type-Order-Theoretic-Join-Semilattice) →
    is-prop (leq-Order-Theoretic-Join-Semilattice x y)
  is-prop-leq-Order-Theoretic-Join-Semilattice =
    is-prop-leq-Poset poset-Order-Theoretic-Join-Semilattice

  refl-leq-Order-Theoretic-Join-Semilattice :
    (x : type-Order-Theoretic-Join-Semilattice) →
    leq-Order-Theoretic-Join-Semilattice x x
  refl-leq-Order-Theoretic-Join-Semilattice =
    refl-leq-Poset poset-Order-Theoretic-Join-Semilattice

  antisymmetric-leq-Order-Theoretic-Join-Semilattice :
    {x y : type-Order-Theoretic-Join-Semilattice} →
    leq-Order-Theoretic-Join-Semilattice x y →
    leq-Order-Theoretic-Join-Semilattice y x →
    x ＝ y
  antisymmetric-leq-Order-Theoretic-Join-Semilattice {x} {y} =
    antisymmetric-leq-Poset poset-Order-Theoretic-Join-Semilattice x y

  transitive-leq-Order-Theoretic-Join-Semilattice :
    (x y z : type-Order-Theoretic-Join-Semilattice) →
    leq-Order-Theoretic-Join-Semilattice y z →
    leq-Order-Theoretic-Join-Semilattice x y →
    leq-Order-Theoretic-Join-Semilattice x z
  transitive-leq-Order-Theoretic-Join-Semilattice =
    transitive-leq-Poset poset-Order-Theoretic-Join-Semilattice

  is-join-semilattice-Order-Theoretic-Join-Semilattice :
    is-join-semilattice-Poset poset-Order-Theoretic-Join-Semilattice
  is-join-semilattice-Order-Theoretic-Join-Semilattice = pr2 A

  join-Order-Theoretic-Join-Semilattice :
    (x y : type-Order-Theoretic-Join-Semilattice) →
    type-Order-Theoretic-Join-Semilattice
  join-Order-Theoretic-Join-Semilattice =
    join-is-join-semilattice-Poset
      poset-Order-Theoretic-Join-Semilattice
      is-join-semilattice-Order-Theoretic-Join-Semilattice

  private
    _∨_ = join-Order-Theoretic-Join-Semilattice

  is-least-binary-upper-bound-join-Order-Theoretic-Join-Semilattice :
    (x y : type-Order-Theoretic-Join-Semilattice) →
    is-least-binary-upper-bound-Poset
      ( poset-Order-Theoretic-Join-Semilattice)
      ( x)
      ( y)
      ( x ∨ y)
  is-least-binary-upper-bound-join-Order-Theoretic-Join-Semilattice =
    is-least-binary-upper-bound-join-is-join-semilattice-Poset
      poset-Order-Theoretic-Join-Semilattice
      is-join-semilattice-Order-Theoretic-Join-Semilattice

  is-binary-upper-bound-join-Order-Theoretic-Join-Semilattice :
    (x y : type-Order-Theoretic-Join-Semilattice) →
    is-binary-upper-bound-Poset
      ( poset-Order-Theoretic-Join-Semilattice)
      ( x)
      ( y)
      ( x ∨ y)
  is-binary-upper-bound-join-Order-Theoretic-Join-Semilattice x y =
    is-binary-upper-bound-is-least-binary-upper-bound-Poset
      ( poset-Order-Theoretic-Join-Semilattice)
      ( is-least-binary-upper-bound-join-Order-Theoretic-Join-Semilattice
        ( x)
        ( y))

  leq-left-join-Order-Theoretic-Join-Semilattice :
    (x y : type-Order-Theoretic-Join-Semilattice) →
    leq-Order-Theoretic-Join-Semilattice x (x ∨ y)
  leq-left-join-Order-Theoretic-Join-Semilattice x y =
    leq-left-is-binary-upper-bound-Poset
      ( poset-Order-Theoretic-Join-Semilattice)
      ( is-binary-upper-bound-join-Order-Theoretic-Join-Semilattice x y)

  leq-right-join-Order-Theoretic-Join-Semilattice :
    (x y : type-Order-Theoretic-Join-Semilattice) →
    leq-Order-Theoretic-Join-Semilattice y (x ∨ y)
  leq-right-join-Order-Theoretic-Join-Semilattice x y =
    leq-right-is-binary-upper-bound-Poset
      ( poset-Order-Theoretic-Join-Semilattice)
      ( is-binary-upper-bound-join-Order-Theoretic-Join-Semilattice x y)

  leq-join-Order-Theoretic-Join-Semilattice :
    {x y z : type-Order-Theoretic-Join-Semilattice} →
    leq-Order-Theoretic-Join-Semilattice x z →
    leq-Order-Theoretic-Join-Semilattice y z →
    leq-Order-Theoretic-Join-Semilattice (x ∨ y) z
  leq-join-Order-Theoretic-Join-Semilattice {x} {y} {z} H K =
    forward-implication
      ( is-least-binary-upper-bound-join-Order-Theoretic-Join-Semilattice
        ( x)
        ( y)
        ( z))
      ( H , K)

Properties

The join operation of order theoretic join-semilattices is associative

module _
  {l1 l2 : Level} (A : Order-Theoretic-Join-Semilattice l1 l2)
  (x y z : type-Order-Theoretic-Join-Semilattice A)
  where

  private
    _∨_ = join-Order-Theoretic-Join-Semilattice A
    _≤_ = leq-Order-Theoretic-Join-Semilattice A

  leq-left-triple-join-Order-Theoretic-Join-Semilattice :
    x ≤ ((x ∨ y) ∨ z)
  leq-left-triple-join-Order-Theoretic-Join-Semilattice =
    calculate-in-Poset
      ( poset-Order-Theoretic-Join-Semilattice A)
      chain-of-inequalities
        x ≤ x ∨ y
            by leq-left-join-Order-Theoretic-Join-Semilattice A x y
            in-Poset poset-Order-Theoretic-Join-Semilattice A
          ≤ (x ∨ y) ∨ z
            by leq-left-join-Order-Theoretic-Join-Semilattice A (x ∨ y) z
            in-Poset poset-Order-Theoretic-Join-Semilattice A

  leq-center-triple-join-Order-Theoretic-Join-Semilattice :
    y ≤ ((x ∨ y) ∨ z)
  leq-center-triple-join-Order-Theoretic-Join-Semilattice =
    calculate-in-Poset
      ( poset-Order-Theoretic-Join-Semilattice A)
      chain-of-inequalities
        y ≤ x ∨ y
            by leq-right-join-Order-Theoretic-Join-Semilattice A x y
            in-Poset poset-Order-Theoretic-Join-Semilattice A
          ≤ (x ∨ y) ∨ z
            by leq-left-join-Order-Theoretic-Join-Semilattice A (x ∨ y) z
            in-Poset poset-Order-Theoretic-Join-Semilattice A

  leq-right-triple-join-Order-Theoretic-Join-Semilattice :
    z ≤ ((x ∨ y) ∨ z)
  leq-right-triple-join-Order-Theoretic-Join-Semilattice =
    leq-right-join-Order-Theoretic-Join-Semilattice A (x ∨ y) z

  leq-left-triple-join-Order-Theoretic-Join-Semilattice' :
    x ≤ (x ∨ (y ∨ z))
  leq-left-triple-join-Order-Theoretic-Join-Semilattice' =
    leq-left-join-Order-Theoretic-Join-Semilattice A x (y ∨ z)

  leq-center-triple-join-Order-Theoretic-Join-Semilattice' :
    y ≤ (x ∨ (y ∨ z))
  leq-center-triple-join-Order-Theoretic-Join-Semilattice' =
    calculate-in-Poset
      ( poset-Order-Theoretic-Join-Semilattice A)
      chain-of-inequalities
        y ≤ y ∨ z
            by leq-left-join-Order-Theoretic-Join-Semilattice A y z
            in-Poset poset-Order-Theoretic-Join-Semilattice A
          ≤ x ∨ (y ∨ z)
            by leq-right-join-Order-Theoretic-Join-Semilattice A x (y ∨ z)
            in-Poset poset-Order-Theoretic-Join-Semilattice A

  leq-right-triple-join-Order-Theoretic-Join-Semilattice' :
    z ≤ (x ∨ (y ∨ z))
  leq-right-triple-join-Order-Theoretic-Join-Semilattice' =
    calculate-in-Poset
      ( poset-Order-Theoretic-Join-Semilattice A)
      chain-of-inequalities
        z ≤ y ∨ z
            by leq-right-join-Order-Theoretic-Join-Semilattice A y z
            in-Poset poset-Order-Theoretic-Join-Semilattice A
          ≤ x ∨ (y ∨ z)
            by leq-right-join-Order-Theoretic-Join-Semilattice A x (y ∨ z)
            in-Poset poset-Order-Theoretic-Join-Semilattice A

  leq-associative-join-Order-Theoretic-Join-Semilattice :
    ((x ∨ y) ∨ z) ≤ (x ∨ (y ∨ z))
  leq-associative-join-Order-Theoretic-Join-Semilattice =
    leq-join-Order-Theoretic-Join-Semilattice A
      ( leq-join-Order-Theoretic-Join-Semilattice A
        ( leq-left-triple-join-Order-Theoretic-Join-Semilattice')
        ( leq-center-triple-join-Order-Theoretic-Join-Semilattice'))
      ( leq-right-triple-join-Order-Theoretic-Join-Semilattice')

  leq-associative-join-Order-Theoretic-Join-Semilattice' :
    (x ∨ (y ∨ z)) ≤ ((x ∨ y) ∨ z)
  leq-associative-join-Order-Theoretic-Join-Semilattice' =
    leq-join-Order-Theoretic-Join-Semilattice A
      ( leq-left-triple-join-Order-Theoretic-Join-Semilattice)
      ( leq-join-Order-Theoretic-Join-Semilattice A
        ( leq-center-triple-join-Order-Theoretic-Join-Semilattice)
        ( leq-right-triple-join-Order-Theoretic-Join-Semilattice))

  associative-join-Order-Theoretic-Join-Semilattice :
    ((x ∨ y) ∨ z) ＝ (x ∨ (y ∨ z))
  associative-join-Order-Theoretic-Join-Semilattice =
    antisymmetric-leq-Order-Theoretic-Join-Semilattice A
      leq-associative-join-Order-Theoretic-Join-Semilattice
      leq-associative-join-Order-Theoretic-Join-Semilattice'

The join operation of order theoretic join-semilattices is commutative

module _
  {l1 l2 : Level} (A : Order-Theoretic-Join-Semilattice l1 l2)
  (x y : type-Order-Theoretic-Join-Semilattice A)
  where

  private
    _∨_ = join-Order-Theoretic-Join-Semilattice A
    _≤_ = leq-Order-Theoretic-Join-Semilattice A

  leq-commutative-join-Order-Theoretic-Join-Semilattice :
    (x ∨ y) ≤ (y ∨ x)
  leq-commutative-join-Order-Theoretic-Join-Semilattice =
    leq-join-Order-Theoretic-Join-Semilattice A
      ( leq-right-join-Order-Theoretic-Join-Semilattice A y x)
      ( leq-left-join-Order-Theoretic-Join-Semilattice A y x)

  leq-commutative-join-Order-Theoretic-Join-Semilattice' :
    (y ∨ x) ≤ (x ∨ y)
  leq-commutative-join-Order-Theoretic-Join-Semilattice' =
    leq-join-Order-Theoretic-Join-Semilattice A
      ( leq-right-join-Order-Theoretic-Join-Semilattice A x y)
      ( leq-left-join-Order-Theoretic-Join-Semilattice A x y)

  commutative-join-Order-Theoretic-Join-Semilattice :
    (x ∨ y) ＝ (y ∨ x)
  commutative-join-Order-Theoretic-Join-Semilattice =
    antisymmetric-leq-Order-Theoretic-Join-Semilattice A
      leq-commutative-join-Order-Theoretic-Join-Semilattice
      leq-commutative-join-Order-Theoretic-Join-Semilattice'

The join operation of order theoretic join-semilattices is idempotent

module _
  {l1 l2 : Level} (A : Order-Theoretic-Join-Semilattice l1 l2)
  (x : type-Order-Theoretic-Join-Semilattice A)
  where

  private
    _∨_ = join-Order-Theoretic-Join-Semilattice A
    _≤_ = leq-Order-Theoretic-Join-Semilattice A

  idempotent-join-Order-Theoretic-Join-Semilattice :
    (x ∨ x) ＝ x
  idempotent-join-Order-Theoretic-Join-Semilattice =
    antisymmetric-leq-Order-Theoretic-Join-Semilattice A
      ( leq-join-Order-Theoretic-Join-Semilattice A
        ( refl-leq-Order-Theoretic-Join-Semilattice A x)
        ( refl-leq-Order-Theoretic-Join-Semilattice A x))
      ( leq-left-join-Order-Theoretic-Join-Semilattice A x x)

Any order theoretic join-semilattice is an algebraic join semilattice

module _
  {l1 l2 : Level} (A : Order-Theoretic-Join-Semilattice l1 l2)
  where

  semigroup-Order-Theoretic-Join-Semilattice : Semigroup l1
  pr1 semigroup-Order-Theoretic-Join-Semilattice =
    set-Order-Theoretic-Join-Semilattice A
  pr1 (pr2 semigroup-Order-Theoretic-Join-Semilattice) =
    join-Order-Theoretic-Join-Semilattice A
  pr2 (pr2 semigroup-Order-Theoretic-Join-Semilattice) =
    associative-join-Order-Theoretic-Join-Semilattice A

  join-semilattice-Order-Theoretic-Join-Semilattice :
    Join-Semilattice l1
  pr1 join-semilattice-Order-Theoretic-Join-Semilattice =
    semigroup-Order-Theoretic-Join-Semilattice
  pr1 (pr2 join-semilattice-Order-Theoretic-Join-Semilattice) =
    commutative-join-Order-Theoretic-Join-Semilattice A
  pr2 (pr2 join-semilattice-Order-Theoretic-Join-Semilattice) =
    idempotent-join-Order-Theoretic-Join-Semilattice A