{-# OPTIONS --universe-polymorphism #-}
-- A proof (of arguably completeness) that the functor
--
-- (─)A : Sets^C → Sets
-- (F)A = FA
--
-- has a right adjoint if C is a discrete category
-- A discrete category can be regarded as a set. Objects of C are the
-- elements, and the fact that there exist only identity morphisms
-- is rougly equivalent to equality of elements, in that
--
-- Hom(A,B) is empty if A ≠ B, and is {id_A} if A = B
--
-- Thus, here, C is taken as a type, and the built-in equality A ≡ B is
-- used instead of Hom(A,B)
module CExp (C : Set) where
open import Level
data _≡_ {i} {A : Set i} (x : A) : A → Set where
refl : x ≡ x
-- Assume that equality of functions is extensional─if f and g agree on
-- all arguments, then they are equal. This is not given in Agda, but
-- is true in set theory.
postulate
ext : ∀{F : C → Set} {A} {B : Set} → {f g : (X : C) → F X → X ≡ A → B}
→ (∀ X FX eq → f X FX eq ≡ g X FX eq) → f ≡ g
-- The (─)A functor, F ↦ FA
─ : C → (C → Set) → Set
(─)A F = F A
-- Natural transformations between two C → Set functors. Technically
-- we should include some naturality conditions, but we'll dispense with
-- that extra work.
_⇒_ : (C → Set) → (C → Set) → Set
F ⇒ G = ∀ X → F X → G X
-- The proposed right adjoint to (─)A
--
-- G A : Sets → Sets^C
-- G A B X = Hom(Hom(X,A),B)
--
-- Here we use X ≡ A instead of Hom(X,A), because the category is
-- discrete, and thus:
--
-- G A B A = Hom({⋆}, B)
-- G A B X = Hom({} , B) for A ≠ X
G : C → Set → (C → Set)
G A B X = X ≡ A → B
-- This is a helper function for the left-to-right part of the
-- adjunction. It takes the morphism f : FA → B and returns the
-- natural transformation φ : F ⇒ G A B. All the components of
-- the transformation except for the A component simply produce
-- the empty function, while the A component produces f.
--
-- In category theory, this would be something like
--
-- blip A F B f X FX g = (f ∘ Fg) FX
--
-- since
--
-- g : X → A
-- f : FA → B
-- f ∘ Fg : FX → B
--
-- And then the proof in aux would of course be different.
blip : ∀ A F (B : Set) (f : (─)A F → B) → (F ⇒ G A B)
blip A F B f .A FA refl = f FA
-- isomorphisms of sets
record _≅_ (A B : Set) : Set where
field
♯ : A → B
♭ : B → A
iso⇒ : ∀ x → ♭ (♯ x) ≡ x
iso⇐ : ∀ y → ♯ (♭ y) ≡ y
-- Adjunctions (specialized to the types we care about in this example
-- for simplicity).
_⊣_ : ((C → Set) → Set) → (Set → (C → Set)) → Set₁
G ⊣ H = ∀ F B → (G F → B) ≅ (F ⇒ H B)
-- The isomorphism component of the adjunction proof. Technically again
-- we should show that the isomorphism is natural in F and B, but that's
-- a lot of extra modeling work.
adj : ∀ A → (─)A ⊣ G A
adj A F B = record { ♯ = λ f → blip A F B f
; ♭ = λ φ FA → φ A FA refl
; iso⇒ = λ _ → refl
; iso⇐ = λ φ → ext (aux φ)
}
where
-- Here we observe that the only non-empty case for X ≡ A is refl : A ≡ A,
-- and so our isomorphism preserves 'natural transformations'. In the
-- category theoretic version, this would correspond (I believe) to
-- observing that Hom(X,A) is either empty or contains only an identity.
-- So, when X = A
--
-- φ_A : FA → G A B A = FA → Hom({id_A},B)
--
-- and when X ≠ A
--
-- φ_X : FX → Hom({},B)
--
-- So, φ is fully determined by its value at A, because all other cases
-- are trivial. Further, B^{id_A} is isomorphic to B, so φ_A must be
-- equivalent to a morphism FA → B, which is what we have on the other
-- side of the isomorphism. Thus, with some hand waving, a round trip
-- through our isomorphism preserves the only non-trivial pieces of
-- information we have, probably making use of the fact that:
--
-- φ_A ∘ Fid_A = φ_A ∘ id_FA = φ_A
--
-- and id_A is the only thing inhabiting Hom(A,A).
aux : ∀(φ : ∀ X → F X → X ≡ A → B) X (FX : F X) (eq : X ≡ A)
→ blip A F B (λ FA → φ A FA refl) X FX eq ≡ φ X FX eq
aux φ .A FA refl = refl