Chuangjie Xu 2013 (updated in February 2015)

\begin{code}

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

module UsingIrrelevantFunext.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 UsingIrrelevantFunext.Irrelevance
open import UsingIrrelevantFunext.Space.Coverage
open import UsingIrrelevantFunext.Space.Space
open import UsingIrrelevantFunext.Space.CartesianClosedness
open import UsingIrrelevantFunext.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 : ₂ℕ  ₂ℕ)  r  C 
     Σ \(φ : ₂ℕ  U (ℕSpace  ₂Space))  φ  Probe (ℕSpace  ₂Space)
Lemma[₂ℕ→₂ℕ-to-₂ℕ→ℕ⇒₂] r ucr = φ , prf
 where
  φ : ₂ℕ  U (ℕSpace  ₂Space)
  φ α = r α , Lemma[discrete-ℕSpace] ₂Space (r α)
  prf : ∀(p : ₂ℕ  )  p  LC  ∀(t : ₂ℕ  ₂ℕ)  t  C 
          α  (pr₁  φ)(t α)(p α))  LC
  prf p ucp t uct = Lemma[LM-₂-least-modulus] q l pr
   where
    q : ₂ℕ  
    q α = (pr₁  φ)(t α)(p α)
    m : 
    m = pr₁ ucp
    f : ₂Fin m  
    f s = p (cons s )
    eq : ∀(α : ₂ℕ)  p α  f (take m α)
    eq α = pr₁ (pr₂ ucp) α (cons (take m α) ) (Lemma[cons-take-≡[]] m α )
    k' : 
    k' = pr₁ (max-fin f)
    k'-max : ∀(α : ₂ℕ)  p α  k'
    k'-max α = transport  i  i  k') ((eq α) ⁻¹) (pr₂ (max-fin f) (take m α))
    k : 
    k = succ k'
    k-max : ∀(α : ₂ℕ)  p α < k
    k-max α = ≤-succ (k'-max α)
    ucrt : uniformly-continuous-₂ℕ (r  t)
    ucrt = Lemma[∘-UC] r ucr t uct
    n : 
    n = pr₁ (ucrt 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
    pr : ∀(α β : ₂ℕ)  α ≡[ l ] β  r(t α)(p α)  r(t β)(p β)
    pr α β awl = transport  i  r(t α)(p α)  r(t β) i) eqp subgoal
     where
      awm : α ≡[ m ] β
      awm = Lemma[≡[]-≤] awl m≤l
      eqp : p α  p β
      eqp = pr₁ (pr₂ ucp) α β awm
      awn : α ≡[ n ] β
      awn = Lemma[≡[]-≤] awl n≤l
      awk : r (t α) ≡[ k ] r (t β)
      awk = pr₁ (pr₂ (ucrt k)) α β awn
      subgoal : r(t α)(p α)  r(t β)(p α)
      subgoal = Lemma[≡[]-<] awk (p α) (k-max α)

\end{code}

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

\begin{code}

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

Lemma[ID-[≡]] : ∀(α : U (ℕSpace  ₂Space))  [ α  ID (pr₁ α) ]
Lemma[ID-[≡]] α = Lemma[Map-₂-[≡]] ℕSpace α (ID (pr₁ α))  _  refl)

ID-is-a-probe : ID  Probe(ℕSpace  ₂Space)
ID-is-a-probe = pr₂ (Lemma[₂ℕ→₂ℕ-to-₂ℕ→ℕ⇒₂] id 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 : ₂ℕ  U X)  p  Probe X
Lemma[Yoneda] X (f , cts) = (f  ID) , (cts ID ID-is-a-probe)

\end{code}