module Order.Diagram.Join.Reasoning
  {o β„“} {P : Poset o β„“} {_βˆͺ_ : ⌞ P ⌟ β†’ ⌞ P ⌟ β†’ ⌞ P ⌟}
  (βˆͺ-joins : βˆ€ x y β†’ is-join P x y (x βˆͺ y))

Reasoning about joinsπŸ”—

This module provides syntax and reasoning combinators for working with partial orders that have all joins.

joins : βˆ€ x y β†’ Join P x y
joins x y .lub      = x βˆͺ y
joins x y .has-join = βˆͺ-joins x y

module joins {x} {y} = Join (joins x y)
open joins renaming
  ( l≀join to l≀βˆͺ
  ; r≀join to r≀βˆͺ
  ; least to βˆͺ-universal)

The join operation is idempotent and commutative.

  βˆͺ-idem : βˆ€ {x} β†’ x βˆͺ x ≑ x
  βˆͺ-idem = ≀-antisym (βˆͺ-universal _ ≀-refl ≀-refl) l≀βˆͺ

  βˆͺ-comm : βˆ€ {x y} β†’ x βˆͺ y ≑ y βˆͺ x
  βˆͺ-comm =
      (βˆͺ-universal _ r≀βˆͺ l≀βˆͺ)
      (βˆͺ-universal _ r≀βˆͺ l≀βˆͺ)

Furthermore, it is associative, and thus forms a semigroup.

  βˆͺ-assoc : βˆ€ {x y z} β†’ x βˆͺ (y βˆͺ z) ≑ (x βˆͺ y) βˆͺ z
  βˆͺ-assoc =
      (βˆͺ-universal _
        (≀-trans l≀βˆͺ l≀βˆͺ)
        (βˆͺ-universal _ (≀-trans r≀βˆͺ l≀βˆͺ) r≀βˆͺ))
      (βˆͺ-universal _
        (βˆͺ-universal _ l≀βˆͺ (≀-trans l≀βˆͺ r≀βˆͺ))
        (≀-trans r≀βˆͺ r≀βˆͺ))

  βˆͺ-is-semigroup : is-semigroup _βˆͺ_
  βˆͺ-is-semigroup .has-is-magma .has-is-set = Ob-is-set
  βˆͺ-is-semigroup .associative = βˆͺ-assoc

Additionally, it respects the ordering on in each variable.

    : βˆ€ {x y x' y'}
    β†’ x ≀ x'
    β†’ y ≀ y'
    β†’ (x βˆͺ y) ≀ (x' βˆͺ y')
  βˆͺ≀βˆͺ p q = βˆͺ-universal _ (≀-trans p l≀βˆͺ) (≀-trans q r≀βˆͺ)

Finally, we note that the join operation determines the order on as witnessed by the following equivalence.

  βˆͺβ†’order : βˆ€ {x y} β†’ x βˆͺ y ≑ y β†’ x ≀ y
  βˆͺβ†’order {x} {y} p =
    x       β‰€βŸ¨ l≀βˆͺ βŸ©β‰€
    (x βˆͺ y) =⟨ p ⟩=
    y       β‰€βˆŽ

  orderβ†’βˆͺ : βˆ€ {x y} β†’ x ≀ y β†’ x βˆͺ y ≑ y
  orderβ†’βˆͺ p = ≀-antisym (βˆͺ-universal _ p ≀-refl) r≀βˆͺ

  βˆͺ≃order : βˆ€ {x y} β†’ (x βˆͺ y ≑ y) ≃ (x ≀ y)
  βˆͺ≃order = prop-ext! βˆͺβ†’order orderβ†’βˆͺ