open import Algebra.Semigroup
open import Algebra.Magma

open import Cat.Prelude

open import Order.Diagram.Join
open import Order.Base

import Order.Reasoning

module Order.Diagram.Join.Reasoning
{o β} {P : Poset o β} {_βͺ_ : β P β β β P β β β P β}
(βͺ-joins : β x y β is-join P x y (x βͺ y))
where

open Order.Reasoning P
open Join


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


The join operation is idempotent and commutative.

abstract
βͺ-idem : β {x} β x βͺ x β‘ x
βͺ-idem = β€-antisym (βͺ-universal _ β€-refl β€-refl) lβ€βͺ

βͺ-comm : β {x y} β x βͺ y β‘ y βͺ x
βͺ-comm =
β€-antisym
(βͺ-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 =
β€-antisym
(βͺ-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β€βͺ)

  βͺβ€βͺl : β {x y x'} β x β€ x' β (x βͺ y) β€ (x' βͺ y)
βͺβ€βͺl p = βͺβ€βͺ p β€-refl

βͺβ€βͺr : β {x y y'} β y β€ y' β (x βͺ y) β€ (x βͺ y')
βͺβ€βͺr p = βͺβ€βͺ β€-refl p


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 =