πŸ“₯ Download raw
{-# OPTIONS --cubical-compatible #-}
module Padova2025.Explorations.Uncountability.Impossible.Toy where

open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProgrammingBasics.HigherOrder
open import Padova2025.ProvingBasics.Termination.Gas
open import Padova2025.Explorations.Uncountability.Applications

_β—‚_ : Bool β†’ Cantor β†’ Cantor
x β—‚ xs = Ξ» { zero β†’ x ; (succ n) β†’ xs n }

{-# NON_TERMINATING #-}
Ξ΅ : (Cantor β†’ Bool) β†’ Cantor
Ξ΅ P = x β—‚ Ξ΅ (P ∘ (x β—‚_))
  where
  x : Bool
  x = P (false β—‚ Ξ΅ (P ∘ (false β—‚_)))

has-root? : (Cantor β†’ Bool) β†’ Bool
has-root? P = not (P (Ξ΅ P))

root : (Cantor β†’ Bool) β†’ Maybe (List Bool)
root P with P (Ξ΅ P)
... | false = just (map (Ρ P) (zero ∷ one ∷ two ∷ three ∷ four ∷ []))
... | true  = nothing

_≑?_ : (Cantor β†’ Bool) β†’ (Cantor β†’ Bool) β†’ Bool
P ≑? Q = not (has-root? (Ξ» xs β†’ not (xor (P xs) (Q xs))))
  where
  xor : Bool β†’ Bool β†’ Bool
  xor false false = false
  xor false true  = true
  xor true  false = true
  xor true  true  = false