module Algebra.Lattice.JoinSemilattice
import public Builtin
import public Algebra.Relation.Order
%default total
infixl 5 \/
public export
interface Order t => JoinSemilattice t where
  (\/) : t -> t -> t
  proofIdempotence : (x : t) -> x \/ x = x
  proofCommutative : (x, y : t) -> x \/ y = y \/ x
  proofAssocitive : (x, y, z : t) -> x \/ (y \/ z) = (x \/ y) \/ z
  proofUpperBound : (x, y : t) -> (x `LTE` x \/ y, y `LTE` x \/ y)
  proofLeastUpperBound : (b, x, y : t) -> x `LTE` b -> y `LTE` b ->  x \/ y `LTE` b

module Algebra.Lattice.MeetSemilattice
import public Builtin
import public Algebra.Relation.Order
%default total
infixl 5 /\
public export
interface Order t => MeetSemilattice t where
  (/\) : t -> t -> t
  proofIdempotence : (x : t) -> x /\ x = x
  proofCommutative : (x, y : t) -> x /\ y = y /\ x
  proofAssocitive : (x, y, z : t) -> x /\ (y /\ z) = (x /\ y) /\ z
  proofLowerBound : (x, y : t) -> (x /\ y `LTE` x, x /\ y `LTE` y)
  proofGreatestLowerBound : (b, x, y : t) -> b `LTE` x -> b `LTE` y -> b `LTE` x /\ y

	, Algebra.Lattice.JoinSemilattice
	, Algebra.Lattice.MeetSemilattice