open import Cat.Prelude

open import Order.Diagram.Lub.Reasoning
open import Order.Lattice.Distributive
open import Order.Semilattice.Join
open import Order.Semilattice.Meet
open import Order.Diagram.Glb
open import Order.Diagram.Lub
open import Order.Lattice
open import Order.Frame
open import Order.Base

import Order.Semilattice.Join.Reasoning
import Order.Semilattice.Meet.Reasoning
import Order.Lattice.Reasoning
import Order.Reasoning

module Order.Frame.Reasoning {o β} {P : Poset o β} (frm : is-frame P) where

open Order.Reasoning P public
open is-frame frm hiding (meets ; joins) public


This module exposes a large collection of reasoning combinators for working with frames, along with re-exporting tools for working with the underlying lattice.

meets : Meet-semilattice o β
meets = P , has-meet-slat

joins : Join-semilattice o β
joins = P , has-join-slat

lattice : Lattice o β
lattice = P , has-lattice

open Order.Lattice.Reasoning has-lattice using
; βͺ-idl; βͺ-idr; module βͺ
) public


This module also has further lemmas about the interplay between meets and arbitrary joins. The following result holds in any cocomplete lattice:

β-product
: β {I J : Type o} (F : I β β P β) (G : J β β P β)
β β (Ξ» i β β Ξ» j β G i β© F j)
β‘ β {I = I Γ J} (Ξ» p β F (p .fst) β© G (p .snd))
β-product {I} {J} F G = β€-antisym
(β-universal _ Ξ» j β β-universal _ Ξ» i β
β {I = I Γ J} (Ξ» v β F (v .fst) β© G (v .snd)) β€β)
(β-universal _ Ξ» where
(i , j) β
β (Ξ» i β F i β© G j)         β€β¨ β-inj j β©β€
β (Ξ» i β β Ξ» j β F j β© G i) =β¨ ap β (funext Ξ» i β ap β \$ funext Ξ» j β β©-comm) β©=
β (Ξ» i β β Ξ» j β G i β© F j) β€β)


But this result relies on the cocontinuity of meets.

β-β©-product
: β {I J : Type o} (F : I β β P β) (G : J β β P β)
β β F β© β G
β‘ β {I = I Γ J} (Ξ» i β F (i .fst) β© G (i .snd))
β (Ξ» i β β F β© G i)               β‘β¨ ap β (funext Ξ» i β β©-comm β β-distribl (G i) F) β©β‘
β (Ξ» i β β Ξ» j β G i β© F j)       β‘β¨ β-product F G β©β‘
β (Ξ» i β F (i .fst) β© G (i .snd)) β

β-distribr : β {I} (f : I β Ob) x β β f β© x β‘ β Ξ» i β f i β© x
β-distribr f x =
Β·Β· β-distribl x f
Β·Β· ap β (funext Ξ» _ β β©-comm)


Meets distribute over binary joins, so every frame is a distributive lattice.

opaque
unfolding Lubs._βͺ_