open import Cat.Prelude

open import Data.Sum.Base

open import Order.Diagram.Join
open import Order.Diagram.Meet
open import Order.Lattice
open import Order.Base

import Order.Lattice.Reasoning as Lat
import Order.Reasoning as Pos

module Order.Lattice.Distributive {o β} {P : Poset o β} (l : is-lattice P) where

open Pos P
open Lat l


# Distributive latticesπ

A distributive lattice, as the name implies, is a lattice where the operations of meet and join distribute over each other: that is, for any triple of elements

Rather remarkably, it turns out that either equation implies the other. We provide a pair of parametrised modules which quantifies over one of the equations and proves the other. For convenience, these modules also define distributivity on the right, too; this is a consequence of both meets and joins being commutative operators.

module Distributive where

  module from-β© (β©-distribl : β {x y z} β x β© (y βͺ z) β‘ (x β© y) βͺ (x β© z)) where abstract

βͺ-distribl : β {x y z} β x βͺ (y β© z) β‘ (x βͺ y) β© (x βͺ z)
βͺ-distribl {x} {y} {z} = sym $(x βͺ y) β© (x βͺ z) β‘β¨ β©-distribl β©β‘ ((x βͺ y) β© x) βͺ ((x βͺ y) β© z) β‘β¨ apβ _βͺ_ β©-absorbr refl β©β‘ x βͺ ((x βͺ y) β© z) β‘β¨ apβ _βͺ_ refl β©-distribr β©β‘ x βͺ (x β© z βͺ y β© z) β‘β¨ βͺ-assoc β©β‘ (x βͺ x β© z) βͺ (y β© z) β‘β¨ apβ _βͺ_ βͺ-absorbl refl β©β‘ x βͺ (y β© z) β βͺ-distribr : β {x y z} β (y β© z) βͺ x β‘ (y βͺ x) β© (z βͺ x) βͺ-distribr = βͺ-comm Β·Β· βͺ-distribl Β·Β· apβ _β©_ βͺ-comm βͺ-comm  The construction assuming that join distributes over meet is formally dual.  module from-βͺ (βͺ-distribl : β {x y z} β x βͺ (y β© z) β‘ (x βͺ y) β© (x βͺ z)) where abstract βͺ-distribr : β {x y z} β (y β© z) βͺ x β‘ (y βͺ x) β© (z βͺ x) βͺ-distribr = βͺ-comm Β·Β· βͺ-distribl Β·Β· apβ _β©_ βͺ-comm βͺ-comm β©-distribl : β {x y z} β x β© (y βͺ z) β‘ (x β© y) βͺ (x β© z) β©-distribl {x} {y} {z} = sym$
x β© (y βͺ z)                   β


distrib-leββ©-distribl