Chuangjie Xu 2012 (updated in February 2015)

\begin{code}

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

module UsingSetoid.Space.YonedaLemma where

open import Preliminaries.SetsAndFunctions hiding (_+_)
open import Preliminaries.NaturalNumber
open import Preliminaries.Boolean
open import Preliminaries.Sequence
open import Continuity.UniformContinuity
open import UsingSetoid.Setoid
open import UsingSetoid.Space.Coverage
open import UsingSetoid.Space.Space
open import UsingSetoid.Space.CartesianClosedness
open import UsingSetoid.Space.DiscreteSpace

\end{code}

Because our site is a one-object category, there is only one representable
sheaf, which is concrete and hence can be regarded as a C-space.  This concrete
sheaf, seen as a C-space, is the set ₂ℕ equipped with all uniformly continuous
maps ₂ℕ → ₂ℕ as probes.  Moreover, it is (isomorphic to) the exponential of the
discrete spaces ₂Space and ℕSpace in the category of C-spaces.  The following
lemma is one direction of this fact, which assigns each probe on ₂ℕ, i.e. a
uniformly continuous map, to a probe on the exponential ℕSpace ⇒ ₂Space.

\begin{code}

Lemma[₂ℕ→₂ℕ-to-₂ℕ→ℕ⇒₂] : (r : E-map-₂ℕ-₂ℕ) → r ∈ C →
     Σ \(φ : E-map-₂ℕ (U (ℕSpace ⇒ ₂Space))) → φ ∈ Probe (ℕSpace ⇒ ₂Space)
Lemma[₂ℕ→₂ℕ-to-₂ℕ→ℕ⇒₂] (r , er) rC = (φ , eφ) , prf
 where
  φ : ₂ℕ → G (ℕSpace ⇒ ₂Space)
  φ α = (r α , Lemma[₂ℕ-E-map] (r α)) , 
        Lemma[discrete-ℕSpace] ₂Space (r α , Lemma[₂ℕ-E-map] (r α))
  eφ : ∀ α α' → α ≣ α' → ∀ i → r α i ≡ r α' i
  eφ = er
  prf : ∀ p → p ∈ LC → ∀ t → t ∈ C
      → Exp ℕSpace ₂Space (φ , eφ) t p ∈ LC
  prf (p , ep) (m , pr , _) (t , et) tC = Lemma[LM-₂-least-modulus] q l claim
   where
    q : ₂ℕ → ₂
    q α = r(t α)(p α)
    f : ₂Fin m → ℕ
    f s = p (cons s 0̄)
    eq : ∀ α → p α ≡ f (take m α)
    eq α = pr α (cons (take m α) 0̄) (Lemma[cons-take-≡[]] m α 0̄)
    k : ℕ
    k = succ (pr₁ (max-fin f))
    k-max : ∀ α → p α < k
    k-max α = ≤-succ (transport (λ i → i ≤ pr₁ (max-fin f))
                      ((eq α)⁻¹) (pr₂ (max-fin f) (take m α)))
    rtC : uniformly-continuous-₂ℕ (r ∘ t)
    rtC = Lemma[∘-UC] r rC t tC
    n : ℕ
    n = pr₁ (rtC k)
    l : ℕ
    l = max m n
    m≤l : m ≤ l
    m≤l = max-spec₀ m n
    n≤l : n ≤ l
    n≤l = max-spec₁ m n
    claim : ∀(α β : ₂ℕ) → α ≡[ l ] β → r(t α)(p α) ≡ r(t β)(p β)
    claim α β el = transport (λ i → r(t α)(p α) ≡ r(t β) i) eqp subgoal
     where
      em : α ≡[ m ] β
      em = Lemma[≡[]-≤] el m≤l
      eqp : p α ≡ p β
      eqp = pr α β em
      en : α ≡[ n ] β
      en = Lemma[≡[]-≤] el n≤l
      ek : r (t α) ≡[ k ] r (t β)
      ek = pr₁ (pr₂ (rtC k)) α β en
      subgoal : r(t α)(p α) ≡ r(t β)(p α)
      subgoal = Lemma[≡[]-<] ek (p α) (k-max α)

\end{code}

In particular, the "identity" map ₂ℕ → U(ℕSpace ⇒ ₂Space) is a probe on the
exponential ℕSpace ⇒ ₂Space.

\begin{code}

ID : E-map-₂ℕ (U (ℕSpace ⇒ ₂Space))
ID = pr₁ (Lemma[₂ℕ→₂ℕ-to-₂ℕ→ℕ⇒₂] (E-id E₂ℕ) Lemma[id-UC])

ID-is-a-probe : ID ∈ Probe(ℕSpace ⇒ ₂Space)
ID-is-a-probe = pr₂ (Lemma[₂ℕ→₂ℕ-to-₂ℕ→ℕ⇒₂] (E-id E₂ℕ) Lemma[id-UC])

\end{code}

Using the above facts, we conclude that the Yoneda Lemma amounts to saying that
the set of continuous maps from the exponential ℕSpace ⇒ ₂Space to any C-space X
is isomorphic to the C-topology of X.  The following gives one direction of the
Yoneda Lemma, which is sufficient to construct a fan functional.

\begin{code}

Lemma[Yoneda] : ∀(X : Space) → Map (ℕSpace ⇒ ₂Space) X →
                 Σ \(p : E-map-₂ℕ (U X)) → p ∈ Probe X
Lemma[Yoneda] X (f , cts) = (⟨ U(ℕSpace ⇒ ₂Space) ∣ U X ⟩ f ◎ ID) , (cts ID ID-is-a-probe)

\end{code}