Skip to content

Instantly share code, notes, and snippets.

@Lysxia
Last active March 7, 2024 08:10
  • Star 0 You must be signed in to star a gist
  • Fork 1 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save Lysxia/79846cce777f0394a6f69d84576a325b to your computer and use it in GitHub Desktop.
(∀ {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
{-# 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)
-- 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] ]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment