The initial algebra for the functor X ↦ (X → ∅) → ∅ is ∅.

doubleNegationInitialAlgebra.agda

-- empty type
data 𝟘 : Set where

absurd : {A : Set} → 𝟘 → A
absurd ()

-- booleans
data 𝟚 : Set where
  false true : 𝟚

-- identity type
data _≡_ {A : Set} : A → A → Set where
  refl : (x : A) → x ≡ x

-- function composition
_∘_ : {X Y Z : Set} → (Y → Z) → (X → Y) → (X → Z)
g ∘ f = λ x → g (f x)

-- double exponential
F : Set → Set → Set
F A X = (X → A) → A

-- the initial algebra for F A
record D (A : Set) : Set₁ where
  field
    I : Set -- the carrier
    ι : F A I → I -- the structure map
    ind : (X : Set) → (F A X → X) → I → X -- initiality
    β : (X : Set) → (f : F A X → X) → (h : F A I) → (ind X f (ι h) ≡ f (λ (r : X → A) → h (r ∘ ind X f)))

open D

-- the empty type is an initial F 𝟘 algebra
D-𝟘 : D 𝟘
D-𝟘 = record { I = 𝟘
             ; ι = λ u → u (λ x → x)
             ; ind = λ X f → absurd
             ; β = λ X f h → absurd (h λ x → x)
             }

-- and every initial F 𝟘 algebra is empty
D-is-empty : (T : D 𝟘) → I T → 𝟘
D-is-empty T u = ind T 𝟘 (ι D-𝟘) u