Chuangjie Xu 2014

\begin{code}

{-# OPTIONS --without-K #-}

module CwF.Sheaf.Base where

open import Preliminaries.SetsAndFunctions
open import Preliminaries.NaturalNumber
open import Preliminaries.Sequence
open import Continuity.UniformContinuity
open import UsingFunext.Space.Coverage
open import CwF.Sheaf.Preliminaries

\end{code}

The underlying category of the site is the monoid of uniformly continuous
endomaps on the Cantor space.

For each natural number n, there is a covering family {Cons s}_{s : ₂Fin n}.

\begin{code}

ℂ : Set
ℂ = Σ \(t : ₂ℕ → ₂ℕ) → t ∈ C

Ι : ℂ
Ι = id , Lemma[id-UC]

infixr  _○_

_○_ : ℂ → ℂ → ℂ
(t , uc) ○ (t' , uc') = t ∘ t' , Lemma[∘-UC] t uc t' uc'

Cons : {n : ℕ} → ₂Fin n → ℂ
Cons s = cons s , Lemma[cons-UC] s

\end{code}

Sheaves and natural transformations

\begin{code}

Sheaf : Set₁
Sheaf = Σ \(Γ : Set) →
          Σ \(_•_ : Γ → ℂ → Γ) →
            (hset Γ)
          × (∀(γ : Γ) → (γ • Ι) ≡ γ)
          × (∀(γ : Γ)(t r : ℂ) → ((γ • t) • r) ≡ (γ • (t ○ r)))
          × (∀(n : ℕ)(ρ : ₂Fin n → Γ) → Σ! \(γ : Γ) → ∀ s → (γ • (Cons s)) ≡ ρ s)

Nat : Sheaf → Sheaf → Set
Nat (Γ , _•_ , _) (Δ , _◦_ , _) = Σ \(σ : Γ → Δ) → ∀ γ t → ((σ γ) ◦ t) ≡ (σ (γ • t))

U = pr₁

Act : (Γ : Sheaf) → U Γ → ℂ → U Γ
Act (_ , _•_ , _) = _•_
syntax Act Γ γ t = γ •[ Γ ] t

cond₁ : (Γ : Sheaf)
      → ∀ γ → (γ •[ Γ ] Ι) ≡ γ
cond₁ (_ , _ , _ , c , _) = c

cond₂ : (Γ : Sheaf)
      → ∀ γ t r → ((γ •[ Γ ] t) •[ Γ ] r) ≡ (γ •[ Γ ] (t ○ r))
cond₂ (_ , _ , _ , _ , c , _) = c

cond₃ : (Γ : Sheaf)
      → ∀(n : ℕ)(ρ : ₂Fin n → U Γ) → Σ! \ γ → ∀ s → (γ •[ Γ ] (Cons s)) ≡ ρ s
cond₃ (_ , _ , _ , _ , _ , c) = c

Amal : (Γ : Sheaf) → (n : ℕ) → (₂Fin n → U Γ) → U Γ
Amal Γ n ρ = pr₁(cond₃ Γ n ρ)

Amal-spec : (Γ : Sheaf) → (n : ℕ) → (ρ : ₂Fin n → U Γ)
          → ∀ s → ((Amal Γ n ρ) •[ Γ ] (Cons s)) ≡ (ρ s)
Amal-spec Γ n ρ = pr₁(pr₂(cond₃ Γ n ρ))

Amal-uniq : (Γ : Sheaf) → (n : ℕ) → (ρ : ₂Fin n → U Γ)
          → ∀(γ : U Γ) → (∀ s → (γ •[ Γ ] (Cons s)) ≡ ρ s) → Amal Γ n ρ ≡ γ
Amal-uniq Γ n ρ = pr₂(pr₂(cond₃ Γ n ρ))


⟪_,_,_⟫_◎_ : (Γ Δ Θ : Sheaf) → Nat Δ Γ → Nat Θ Δ → Nat Θ Γ
⟪ Γ , Δ , Θ ⟫ (σ , nσ) ◎ (τ , nτ) = (σ ∘ τ) , (λ θ t → (nσ (τ θ) t) · (ap σ (nτ θ t)))

\end{code}

Contexts are interpreted as sheaves and substitutions as natural
transformations.

\begin{code}

Cxt : Set₁
Cxt = Sheaf

Sub : Cxt → Cxt → Set
Sub = Nat

I : (Γ : Cxt) → Sub Γ Γ
I Γ = (λ γ → γ) , (λ _ _ → refl)

\end{code}

Equations

\begin{code}

-- 1 ∘ σ = σ
Eq₀ : (Γ Δ : Cxt) (σ : Sub Δ Γ)
    → ∀(δ : U Δ) → pr₁(⟪ Γ , Γ , Δ ⟫ I Γ ◎ σ) δ ≡ pr₁ σ δ
Eq₀ Γ Δ σ δ = refl

-- σ ∘ 1 = σ
Eq₁ : (Γ Δ : Cxt) (σ : Sub Δ Γ)
    → ∀(δ : U Δ) → pr₁(⟪ Γ , Δ , Δ ⟫ σ ◎ I Δ) δ ≡ pr₁ σ δ
Eq₁ Γ Δ σ δ = refl

-- (σ ∘ τ) ∘ ν = σ ∘ (τ ∘ ν)
Eq₂ : (Γ Δ Θ Ξ : Cxt) (σ : Sub Δ Γ) (τ : Sub Θ Δ) (ν : Sub Ξ Θ)
    → ∀(ξ : U Ξ) →   pr₁ (⟪ Γ , Θ , Ξ ⟫ (⟪ Γ , Δ , Θ ⟫ σ ◎ τ) ◎ ν) ξ
                   ≡ pr₁ (⟪ Γ , Δ , Ξ ⟫ σ ◎ (⟪ Δ , Θ , Ξ ⟫ τ ◎ ν)) ξ
Eq₂ Γ Δ Θ Ξ σ τ ν χ = refl

\end{code}