<!--
```agda
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
```
-->

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

<!--
```agda
open Frame isf
```
-->

# Frames as sites {defines="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$, 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$. 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
f i$; this is the specialisation to partial orders of the sieve
generated by a family of arrows.

```agda
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$, we can restrict $f$ to a covering of
$V$. The answer is yes, and the process is leaving the index the same,
and intersecting each part of the coverage with $V$. This works only
*because* $X$ is a frame: essentially, if $\bigcup f = U$, 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
$$,
and this last meet, if $V \le U$, is just $V$; so $i \mapsto f(i) \cap
V$ is a covering family for $V$.

```agda
  ∩-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`{.Agda},
we must now show that, if $f$ is a covering family for $U$, then the
intersection $f \cap V$ we computed above is contained in the [[pullback
sieve]] $V^*(f)$. We'll actually do one better: the intersection we
computed *is* the pullback sieve.

```agda
  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|subcanonical coverage]], 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$,
i.e. if its *colimit* is $U$. Regardless, Agda will still ask that we do
a bit of shuffling, and this is where our lemma for simplifying
pullbacks comes in.

```agda
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$; This computation is implicit in the definition
of `∩-covering`{.Agda}, so we may reuse that. In more details, we're
given an object $W$ and a witness $\eps$ that, for every $X \le V$ for
which there exists an $i : I$ with $X \le f(i) \cap V$, we have $X \le
W$, and we must show $V \le W$. Since $\eps$ has a type with pretty
complex quantification, we'll write it out first:

```agda
  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$, it has the
universal property of a join: to show $V \le W$, for any $X$, it
suffices to show that $f(i) \cap V \le W$ for every $i$. By $\eps$, 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$. After this, we can finish the proof by
transitivity.

```agda
      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^*(V)$.

```agda
  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)
```
