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

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)