(∀ {r} → (a → Maybe r) → Maybe r) ≡ ((f : a → Bool) → Maybe (∃[ x ] f x ≡ true)) https://stackoverflow.com/questions/75178350/can-one-simplify-the-codensity-monad-on-maybe

C.agda

{-# OPTIONS --without-K #-}
module C where

open import Function
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; trans; cong; sym)
open import Data.Empty
open import Data.Bool
open import Data.Product as Prod using (∃-syntax; Σ-syntax; _,_; _×_; ∃; proj₁; proj₂)
open import Data.Maybe as Maybe using (Maybe; just; nothing; is-just)
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
open import Axiom.Extensionality.Propositional
open import Axiom.UniquenessOfIdentityProofs

private variable
  a r s : Set

F : Set → Set₁
F a = ∀ {r} → (a → Maybe r) → Maybe r

G : Set → Set
G a = (f : a → Bool) → Maybe (∃[ x ] f x ≡ true)

-- * FtoG

wrap′ : (f : a → Bool) (x : a) (b : Bool) (eq : f x ≡ b) → Maybe (∃[ x ] f x ≡ true)
wrap′ f x true eq = just (x , eq)
wrap′ f x false eq = nothing

wrap : (f : a → Bool) → (a → Maybe (∃[ x ] f x ≡ true))
wrap f x = wrap′ f x (f x) refl

FtoG : F a → G a
FtoG m f = m (wrap f)

-- * GtoF

unwrap : ∀ {f : a → Maybe r} → (∃[ x ] is-just (f x) ≡ true) → r
unwrap {f = f} (x , eq) with f x
... | just y = y

GtoF : G a → F a
GtoF m f = Maybe.map unwrap (m (is-just ∘ f))

-- * Inverse proof

-- The main theorems are FF and GG at the bottom.

-- ** Assumptions: extensionality and parametricity

-- Pointwise-equality implies equality of functions
postulate funext : ∀ {a b} → Extensionality a b

-- Free theorem for F
postulate param_F : (m : F a) → (f : r → s) → (k : a → Maybe r) → Maybe.map f (m k) ≡ m (Maybe.map f ∘ k)

-- Extensionality for implicit functions
ifunext : ∀ {a b} → ExtensionalityImplicit a b
ifunext = implicit-extensionality funext

-- ** Intermediate lemmas

-- Messy, sorry

wrap′-case : (f : a → Bool) (x : a) (b : Bool) (eq : f x ≡ b) → (Σ[ p ∈ f x ≡ true ] wrap′ f x b eq ≡ just (x , p)) ⊎ (f x ≡ false × wrap′ f x b eq ≡ nothing)
wrap′-case f x true eq = inj₁ (eq , refl)
wrap′-case f x false eq = inj₂ (eq , refl)

wrap-case : (f : a → Bool) (x : a) → (Σ[ p ∈ f x ≡ true ] wrap f x ≡ just (x , p)) ⊎ (f x ≡ false × wrap f x ≡ nothing)
wrap-case f x = wrap′-case f x (f x) refl

unwrap-just : (f : a → Maybe r) (x : _) (y : _) → f (proj₁ x) ≡ just y → unwrap {f = f} x ≡ y
unwrap-just f (x , _) y p with f x | p
... | just y | refl = refl

just∘unwrap : (f : a → Maybe r) (x : a) (p : is-just (f x) ≡ true) → just (unwrap {f = f} (x , p)) ≡ f x
just∘unwrap f x p with f x
... | just y = refl

is-just≡false : (f : a → Maybe r) (x : a) → is-just (f x) ≡ false → nothing ≡ f x
is-just≡false f x p with f x
... | nothing = refl

unwrap∘wrap : (f : a → Maybe r) → (x : a) → Maybe.map unwrap (wrap (is-just ∘ f) x) ≡ f x
unwrap∘wrap f x with wrap-case (is-just ∘ f) x
... | inj₁ (p , e) rewrite e = just∘unwrap f x p
... | inj₂ (p , e) rewrite e = is-just≡false f x p

is-just∘wrap′ : (f : a → Bool) (x : a) (b : Bool) (p : f x ≡ b) → is-just (wrap′ f x b p) ≡ f x
is-just∘wrap′ f x true p = sym p
is-just∘wrap′ f x false p = sym p

is-just∘wrap : (f : a → Bool) → is-just ∘ wrap f ≡ f
is-just∘wrap f = funext λ x → is-just∘wrap′ f x (f x) refl

∃-eq : ∀ {A : Set} {P Q : A → Set} (x : ∃ P) (y : ∃ Q) → Set
∃-eq x y = proj₁ x ≡ proj₁ y

data Maybe-eq {A B : Set} (P : A → B → Set) : Maybe A → Maybe B → Set where
  nothing : Maybe-eq P nothing nothing
  just : ∀ {x y} → P x y → Maybe-eq P (just x) (just y)

Maybe-refl : ∀ {A} {P : A → A → Set} → (∀ {x} → P x x) → ∀ {y} → Maybe-eq P y y
Maybe-refl Prefl {nothing} = nothing
Maybe-refl Prefl {just x} = just Prefl

_≈_ : {f g : a → Bool} → Maybe (∃[ x ] f x ≡ true) → Maybe (∃[ x ] g x ≡ true) → Set
_≈_ = Maybe-eq ∃-eq

ext-G : (m : G a) {f g : a → Bool} → f ≡ g → m f ≈ m g
ext-G m refl = Maybe-refl refl

unwrap-G : (f : a → Bool) (x : Maybe (∃[ x ] is-just (wrap f x) ≡ true)) → Maybe.map unwrap x ≈ x
unwrap-G f nothing = nothing
unwrap-G f (just (x , p)) with wrap-case f x
... | inj₁ (e , q) = just (cong proj₁ (unwrap-just (λ x → wrap f x) (_ , _) (x , e) q))
... | inj₂ (e , q) = contra (trans (cong is-just (sym q)) p)
  where
    contra : {A : Set} → false ≡ true → A
    contra ()

sigma-≡ : {A : Set} {P : A → Set} → {p q : ∃ P} → proj₁ p ≡ proj₁ q → (∀ {x} → (e e′ : P x) → e ≡ e′) → p ≡ q
sigma-≡ {p = (_ , p)} {q = (_ , q)} refl f with f p q
... | refl = refl

UIP-Bool : ∀ {b b′ : Bool} → (e e′ : b ≡ b′) → e ≡ e′
UIP-Bool = ≡-irrelevant _≟_
  where open Decidable⇒UIP

≈-≡ : {f : a → Bool} → ∀ {x y} → _≈_ {f = f} {g = f} x y → x ≡ y
≈-≡ nothing = refl
≈-≡ (just p) = cong just (sigma-≡ p UIP-Bool)

≈-trans : ∀ {f g h : a → Bool} {x y z} → _≈_ {f = f} {g = g} x y → _≈_ {f = g} {g = h} y z → _≈_ x z
≈-trans nothing nothing = nothing
≈-trans (just p) (just q) = just (trans p q)

FF' : ∀ (m : F a) (f : a → Maybe r) → GtoF (FtoG m) f ≡ m f
FF' m f = trans (param_F m unwrap _) (cong m (funext λ x → unwrap∘wrap f x))

GG′ : (m : G a) (f : a → Bool) → Maybe.map unwrap (m (is-just ∘ wrap f)) ≈ m f
GG′ m f = ≈-trans (unwrap-G f (m _)) (ext-G m (is-just∘wrap f))

-- * Main theorems

-- FtoG is inverse to GtoF

FF : ∀ (m : F a) → (λ {r} → GtoF (FtoG m) {r}) ≡ m
FF m = ifunext λ {r} → funext λ f → FF' m f

GG : ∀ (m : G a) → FtoG (GtoF m) ≡ m
GG m = funext λ f → ≈-≡ (GG′ m f)

C.hs

-- Cardinality of CodensityT Maybe a for finite type a, with cardinality n
module C where

padAdd :: [Integer] -> [Integer] -> [Integer]
padAdd (x : xs) (y : ys) = x + y : padAdd xs ys
padAdd [] ys = ys
padAdd xs [] = xs

choose :: Integer -> Integer -> Integer
choose = choose'
  where
    choose' n k = (pascal !! fromInteger n) !! fromInteger k
    pascal = [1] : zipWith padAdd pascal (map (0 :) pascal)

f :: Integer -> Integer
f n = product [ (1 + i) ^ choose n i | i <- [1 .. n] ]