open import Cat.Site.Instances.Canonical
open import Cat.Diagram.Colimit.Base
open import Cat.Instances.Elements
open import Cat.Diagram.Sieve
open import Cat.Site.Base
open import Cat.Prelude

open import Order.Diagram.Meet
open import Order.Frame
open import Order.Base
open import Order.Cat

import Order.Frame.Reasoning as Frame

module Cat.Site.Instances.Frame {o ℓ} (X : Poset o ℓ) (isf : is-frame X) where

open Frame isf

Frames as sites🔗

Since sites, as categories we can define sheaves on, are meant to axiomatise what it means for a category to have a notion of covering, we should expect that frames, as geometric objects, should admit the structure of a site.

This module shows that: for a frame $X\text{,}$ thought of as the opens in a space, we say that the coverings for $U:X$ are the families $f:I\to X$ with $\bigcup f=U\text{.}$ To interpret such a family as a sieve, we say that an object $V\le U$ belongs if there exists an $i:I$ with $V\le fi\text{;}$ this is the specialisation to partial orders of the sieve generated by a family of arrows.

private
  Covering : ⌞ X ⌟ → Type _
  Covering U = Σ[ I ∈ Type o ] Σ[ f ∈ (I → ⌞ X ⌟) ] (⋃ f ≡ U)

  generate : ∀ {U} → Covering U → Sieve (poset→category X) U
  generate (I , f , _) .arrows {V} _ = elΩ $ Σ[ i ∈ I ] V ≤ f i
  generate (I , f , _) .closed = rec! λ i α β → inc (i , ≤-trans β α)

For the stability property, we have to check that given a covering $f:I\to U$ and a contained $V\le U\text{,}$ we can restrict $f$ to a covering of $V\text{.}$ The answer is yes, and the process is leaving the index the same, and intersecting each part of the coverage with $V\text{.}$ This works only because $X$ is a frame: essentially, if $\bigcup f=U\text{,}$ then the infinite distributive law gives us $$\left(\bigcup _{i}f(i)\cap V\right)=\left(\bigcup _{i}f(i)\right)\cap V=U\cap V\text{,}$$ and this last meet, if $V\le U\text{,}$ is just $V\text{;}$ so $i\mapsto f(i)\cap V$ is a covering family for $V\text{.}$

  ∩-covering : ∀ {U V} → V ≤ U → Covering U → Covering V
  ∩-covering {U} {V} V≤U (I , f , p) = I , _ , cap-covers where abstract
    cap-covers : ⋃ (λ i → f i ∩ V) ≡ V
    cap-covers =
      ⋃ (λ i → f i ∩ V) ≡˘⟨ ⋃-distribr f V ⟩
      ⋃ f ∩ V           ≡⟨ ap₂ _∩_ p refl ⟩
      U ∩ V             ≡⟨ ∩-comm ∙ order→∩ V≤U ⟩
      V                 ∎

To show that these definitions fit together to give a Coverage, we must now show that, if $f$ is a covering family for $U\text{,}$ then the intersection $f\cap V$ we computed above is contained in the pullback sieve $V^{\ast }(f)\text{.}$ We’ll actually do one better: the intersection we computed is the pullback sieve.

  generate-∩
    : ∀ {U V} (h : V ≤ U) (S : Covering U)
    → generate (∩-covering h S) ≡ pullback h (generate S)
  generate-∩ V≤U (I , f , p) = ext λ {W} W≤V → Ω-ua
    (rec! λ i W≤fi∩V → inc (i , ≤-trans W≤fi∩V ∩≤l))
    (rec! λ i W≤fi   → inc (i , ∩-universal _ W≤fi W≤V))

Open-coverage : Coverage (poset→category X) (lsuc o)
Open-coverage .covers = Covering
Open-coverage .cover = generate
Open-coverage .stable {U} {V} S V≤U = inc (∩-covering V≤U S , incl) where
  incl : generate (∩-covering V≤U S) ⊆ pullback V≤U (generate S)
  incl g = subst (g ∈_) (generate-∩ V≤U S)

The open coverage on a frame enjoys the important property of being subcanonical, i.e. all of its covering sieves are pullback-stable colimits. This is essentially by definition: in the open coverage, a family over $U$ is covering if its union is $U\text{,}$ i.e. if its colimit is $U\text{.}$ Regardless, Agda will still ask that we do a bit of shuffling, and this is where our lemma for simplifying pullbacks comes in.

Open-coverage-is-subcanonical : is-subcanonical _ Open-coverage
Open-coverage-is-subcanonical {U} cov@(I , f , _) {V} V≤U = done where
  open make-is-colimit

  mk : make-is-colim (poset→category X) (generate (∩-covering V≤U cov))
  mk .ψ (elem W (W≤V , _)) = W≤V

In practical terms, all we have to show is that $V$ is the colimit of ${\bigcup }_{i}f(i)\cap V\text{;}$ This computation is implicit in the definition of ∩-covering, so we may reuse that. In more details, we’re given an object $W$ and a witness $\epsilon$ that, for every $X\le V$ for which there exists an $i:I$ with $X\le f(i)\cap V\text{,}$ we have $X\le W\text{,}$ and we must show $V\le W\text{.}$ Since $\epsilon$ has a type with pretty complex quantification, we’ll write it out first:

  mk .universal {W} ε _ =
    let
      ε' : ∀ {X} → X ≤ V → ∃[ i ∈ I ] X ≤ f i ∩ V → X ≤ W
      ε' {X} α β = ε (elem X (α , (tr-□ β)))

Since $V$ is equal to the join ${\bigcup }_{i}f(i)\cap V\text{,}$ it has the universal property of a join: to show $V\le W\text{,}$ for any $X\text{,}$ it suffices to show that $f(i)\cap V\le W$ for every $i\text{.}$ By $\epsilon \text{,}$ we can reduce this to the two trivial conditions $f(i)\cap V\le V$ and $f(i)\cap V\le f(i)\cap V\text{.}$ After this, we can finish the proof by transitivity.

      pt : ∀ i → f i ∩ V ≤ W
      pt i = ε' ∩≤r (inc (i , ≤-refl))
    in
      V                 =˘⟨ ∩-covering V≤U cov .snd .snd ⟩
      ⋃ (λ i → f i ∩ V) ≤⟨ ⋃-universal _ pt ⟩
      W                 ≤∎

Commutativity, universality and uniqueness are all trivial in a poset, so $f\cap V$ is a colim sieve, which is almost what we wanted. The theorem is complete by transporting along our proof that $f\cap V=f^{\ast }(V)\text{.}$

  mk .commutes _       = prop!
  mk .factors  _ _     = prop!
  mk .unique   _ _ _ _ = prop!

  done : is-colim (poset→category X) (pullback V≤U (generate cov))
  done = subst (is-colim (poset→category X)) (generate-∩ V≤U _) (to-is-colimitp mk refl)