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

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)