open import Algebra.Monoid

open import Cat.Instances.Delooping
open import Cat.Prelude

open import Order.Semilattice.Join
open import Order.Base

import Cat.Reasoning

import Order.Reasoning

module Order.Semilattice.Join.Reasoning
{o β} {P : Poset o β} (slat : is-join-semilattice P)
where


# Reasoning about join semilatticesπ

This module proves some basic facts about join semilattices, and exposes reasoning combinators for working with them.

open is-join-semilattice slat public
open Order.Reasoning P public


The bottom element of a join semilattice is both a left and right identity element with respect to joins.

βͺ-idl : β {x} β bot βͺ x β‘ x
βͺ-idl = β€-antisym (βͺ-universal _ Β‘ β€-refl) rβ€βͺ

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


Therefore, every join semilattice is a monoid.

βͺ-is-monoid : is-monoid bot _βͺ_
βͺ-is-monoid .has-is-semigroup = βͺ-is-semigroup
βͺ-is-monoid .idl = βͺ-idl
βͺ-is-monoid .idr = βͺ-idr

βͺ-monoid : Monoid-on β P β
βͺ-monoid .Monoid-on.identity = bot
βͺ-monoid .Monoid-on._β_ = _βͺ_
βͺ-monoid .Monoid-on.has-is-monoid = βͺ-is-monoid

module βͺ = Cat.Reasoning (B βͺ-monoid) hiding (Ob)