Least fixpoint.

Mu.agda

module Mu where

open import Agda.Builtin.Equality
open import Data.Maybe using (Maybe; nothing; just)
open import Data.Nat using (ℕ; zero; suc)

data Mu (F : Set → Set) : Set1 where
  mu : (∀ {A : Set} → (F A → A) → A) → Mu F

record _~_ (A : Set1) (B : Set) : Set1 where
  field
    to   : A → B
    from : B → A
    from-to : ∀ (a : A) → from (to a) ≡ a
    to-from : ∀ (b : B) → to (from b) ≡ b

_ : Mu Maybe ~ ℕ
_ = record
  { to   = to
  ; from = from
  ; from-to = from-to
  ; to-from = to-from
  }
  where
  suc' : Maybe ℕ → ℕ
  suc' nothing  = zero
  suc' (just n) = suc n

  to : Mu Maybe → ℕ
  to (mu f) = f suc'

  from : ℕ → Mu Maybe
  from zero = mu (λ f → f nothing)
  from (suc n) with from n
  ... | mu f = mu (λ f' → f' (just (f f')))

  -- There doesn't seem to be any way of proving this because there is no
  -- guarantee about the behavior of `f`.
  from-to : (a : Mu Maybe) → from (to a) ≡ a
  from-to (mu f) with f suc'
  ... | zero  = ?
  ... | suc n = ?

  to-from : (b : ℕ) → to (from b) ≡ b
  to-from zero    = refl
  to-from (suc n) = ?