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

Reasoning about framesπŸ”—

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 ∩
  ; βˆͺ-idl; βˆͺ-idr; module βˆͺ
  ; ∩-absorbl; ∩-absorbr; βˆͺ-absorbl; βˆͺ-absorbr
  ) 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 β†’
    G j ∩ F i                                       =⟨ ∩-comm ⟩=
    F i ∩ G j                                       β‰€βŸ¨ ⋃-inj (i , j) βŸ©β‰€
    ⋃ {I = I Γ— J} (Ξ» v β†’ F (v .fst) ∩ G (v .snd)) β‰€βˆŽ)
  (⋃-universal _ Ξ» where
    (i , j) β†’
      F i ∩ G j                   β‰€βŸ¨ ⋃-inj i βŸ©β‰€
      ⋃ (Ξ» 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))
⋃-∩-product F G =
  ⋃ F ∩ ⋃ G                         β‰‘βŸ¨ ⋃-distribl (⋃ F) G βŸ©β‰‘
  ⋃ (Ξ» 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)) ∎

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

opaque
  unfolding Lubs._βˆͺ_
  ∩-distribl : βˆ€ {x y z} β†’ x ∩ (y βˆͺ z) ≑ (x ∩ y) βˆͺ (x ∩ z)
  ∩-distribl  =
    ⋃-distribl _ _
    βˆ™ ap ⋃ (funext (Ξ» { (lift true) β†’ refl ; (lift false) β†’ refl }))

open Distributive.from-∩ has-lattice ∩-distribl public