open import Algebra.Semigroup
open import Algebra.Magma

open import Cat.Prelude

open import Order.Diagram.Meet
open import Order.Base

import Order.Reasoning

module Order.Diagram.Meet.Reasoning
{o β} {P : Poset o β} {_β©_ : β P β β β P β β β P β}
(β©-meets : β x y β is-meet P x y (x β© y))
where

open Order.Reasoning P
open Meet


This module provides syntax and reasoning combinators for working with partial orders that have all meets.

meets : β x y β Meet P x y
meets x y .glb      = x β© y
meets x y .has-meet = β©-meets x y

module meets {x} {y} = Meet (meets x y)
open meets renaming
public


The meet operation is idempotent and commutative.

abstract

β€-antisym


Furthermore, it is associative, and thus forms a semigroup.

  β©-assoc : β {x y z} β x β© (y β© z) β‘ (x β© y) β© z
β€-antisym



Additionally, it respects the ordering on in each variable.

  β©β€β©
: β {x y x' y'}
β x β€ x'
β y β€ y'

  β©β€β©l : β {x y x'} β x β€ x' β (x β© y) β€ (x' β© y)



Finally, we note that the meet operation determines the order on as witnessed by the following equivalence.

  β©βorder : β {x y} β x β© y β‘ x β x β€ y