module Order.Semilattice.Meet.Reasoning
  {o } {P : Poset o } (slat : is-meet-semilattice P)
  where

Reasoning about meet semilattices🔗

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

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

The top element of a meet semilattice is both a left and right identity element with respect to meets.

∩-idl :  {x}  top  x  x
∩-idl = ≤-antisym ∩≤r (∩-universal _ ! ≤-refl)

∩-idr :  {x}  x  top  x
∩-idr = ≤-antisym ∩≤l (∩-universal _ ≤-refl !)

Therefore, every meet semilattice is a monoid.

∩-is-monoid : is-monoid top _∩_
∩-is-monoid .has-is-semigroup = ∩-is-semigroup
∩-is-monoid .idl = ∩-idl
∩-is-monoid .idr = ∩-idr

∩-monoid : Monoid-on  P 
∩-monoid .Monoid-on.identity = top
∩-monoid .Monoid-on._⋆_ = _∩_
∩-monoid .Monoid-on.has-is-monoid = ∩-is-monoid

module  = Cat.Reasoning (B ∩-monoid) hiding (Ob)