Least and greatest fixpoints in Agda.

Fix.agda

module Fix where

open import Level using (Level; _⊔_; suc)

module Unit where
  data Unit : Set where
    unit : Unit

  ind : forall (P : Unit -> Set)
    -> P unit
    ---------------------------
    -> forall (u : Unit) -> P u
  ind P Punit unit = Punit

module Bool where
  data Bool : Set where
    true  : Bool
    false : Bool

  ind : forall (P : Bool -> Set)
    -> P true
    -> P false
    ---------------------------
    -> forall (b : Bool) -> P b
  ind P Ptrue Pfalse true  = Ptrue
  ind P Ptrue Pfalse false = Pfalse

module Nat where
  data Nat : Set where
    zero : Nat
    succ : Nat -> Nat

  ind : forall (P : Nat -> Set)
    -> P zero
    -> (forall (n : Nat) -> P n -> P (succ n))
    ------------------------------------------
    -> forall (n : Nat) -> P n
  ind P Pzero Psucc zero     = Pzero
  ind P Pzero Psucc (succ n) = Psucc n (ind P Pzero Psucc n)

module Maybe {l : Level} (A : Set l) where
  data Maybe : Set l where
    just    : A -> Maybe
    nothing : Maybe

  ind : forall {l : Level} {P : Maybe -> Set l}
    -> (forall (a : A) -> P (just a))
    -> P nothing
    ---------------------------------
    -> forall (m : Maybe) -> P m
  ind Pjust Pnothing (just a) = Pjust a
  ind Pjust Pnothing nothing  = Pnothing

module Either {l l' : Level} (A : Set l) (B : Set l') where
  data Either : Set (l ⊔ l') where
    left  : A -> Either
    right : B -> Either

  ind : forall {l : Level} {P : Either -> Set l}
    -> (forall (a : A) -> P (left a))
    -> (forall (b : B) -> P (right b))
    ----------------------------------
    -> forall (e : Either) -> P e
  ind Pleft Pright (left a)  = Pleft a
  ind Pleft Pright (right b) = Pright b

module List {l : Level} (A : Set l) where
  data List : Set l where
    nil  : List
    cons : A -> List -> List

  ind : forall {l : Level} {P : List -> Set l}
    -> P nil
    -> (forall (a : A) (l : List) -> P l -> P (cons a l))
    -----------------------------------------------------
    -> forall (l : List) -> P l
  ind Pnil Pcons nil        = Pnil
  ind Pnil Pcons (cons a l) = Pcons a l (ind Pnil Pcons l)

module Prod {l l' : Level} (A : Set l) (B : Set l') where
  data Prod : Set (l ⊔ l') where
    pair : A -> B -> Prod

  ind : forall {l : Level} {P : Prod -> Set l}
    -> (forall (a : A) (b : B) -> P (pair a b))
    -------------------------------------------
    -> forall (p : Prod) -> P p
  ind Ppair (pair a b) = Ppair a b

module Sigma {l l' : Level} (A : Set l) (P : A -> Set l') where
  data Sigma : Set (l ⊔ l') where
    exist : forall (a : A) -> P a -> Sigma

  ind : forall {l : Level} {P' : Sigma -> Set l}
    -> (forall (a : A) (p : P a) -> P' (exist a p))
    -----------------------------------------------
    -> forall (s : Sigma) -> P' s
  ind Pexist (exist a p) = Pexist a p

module Mu {l l' : Level} (F : Set l -> Set l') where
  data Mu : Set (suc (l ⊔ l')) where
    mu : (forall {A : Set l} -> (F A -> A) -> A) -> Mu

  ind : forall {l' : Level} {P : Mu -> Set l'}
    -> (forall (f : forall {A : Set l} -> (F A -> A) -> A) -> P (mu f))
    -------------------------------------------------------------------
    -> forall (m : Mu) -> P m
  ind Pmu (mu f) = Pmu f

module Nu {l l' : Level} (F : Set l -> Set l') where
  data Nu : Set (suc (l ⊔ l')) where
    nu : forall (A : Set l) -> A -> (A -> F A) -> Nu

  ind : forall {l' : Level} {P : Nu -> Set l'}
    -> (forall (A : Set l) (a : A) (f : A -> F A) -> P (nu A a f))
    --------------------------------------------------------------
    -> forall (n : Nu) -> P n
  ind Pnu (nu A a f) = Pnu A a f

data _==_ {l : Level} {A : Set l} (a : A) : A -> Set where
  refl : a == a

{-# BUILTIN EQUALITY _==_ #-}

record _~_ {l l' : Level} (A : Set l) (B : Set l') : Set (l ⊔ l') where
  field
    to   : A -> B
    from : B -> A
    from-to : forall (a : A) -> from (to a) == a
    to-from : forall (b : B) -> to (from b) == b

module _ where
  open Nat
  open Maybe
  open Mu

  iso : Mu Maybe ~ Nat
  iso = record
    { to   = to
    ; from = from
    ; from-to = from-to
    ; to-from = to-from
    }
    where
    to : Mu Maybe -> Nat
    to (mu f) = f \{ (just n) -> succ n ; nothing -> zero }

    from : Nat -> Mu Maybe
    from zero     = mu (\ f -> f nothing)
    from (succ n) with from n
    ... | mu f = mu (\ f' -> f' (just (f f')))

    from-to : (a : Mu Maybe) → from (to a) == a
    from-to (mu f) with f \{ (just n) -> succ n ; nothing -> zero }
    ... | zero   = ?
    ... | succ n = ?

    to-from : (b : Nat) → to (from b) == b
    to-from zero                       = refl
    to-from (succ n) rewrite to-from n = ?