module Ind where

  data Nat : Set where
    Z : Nat
    S : Nat -> Nat

  data Maybe (A : Set) : Set where
    Some : A -> Maybe A
    None : Maybe A

  data Σ (A : Set) (B : A -> Set) : Set where
    _,_ : (x : A) -> B x -> Σ A B

  fst : {A : Set} {B : A -> Set} -> Σ A B -> A
  fst (x , y) = x

  snd : {A : Set} {B : A -> Set} -> (p : Σ A B) -> (B (fst p))
  snd (x , y) = y

  data Id {A : Set} : A -> A -> Set where
    Refl : {N : A} -> Id N N

  subst : {A : Set} {M N : A} (P : A -> Set) -> Id M N -> P M -> P N
  subst P Refl x = x

  resp : {A B : Set} {M N : A} (f : A -> B) -> Id M N -> Id (f M) (f N)
  resp P Refl = Refl

  trans : {A : Set} { M N P : A} -> Id M N -> Id N P -> Id M P
  trans Refl Refl = Refl

  module Alg (P : Nat -> Set) (base : (P Z)) (step : ((n : Nat) -> P n -> P (S n))) where

    myalgebra : Maybe (Σ Nat (\n -> P n)) 
               -> (Σ Nat (\n -> P n))
    myalgebra None = Z , base
    myalgebra (Some pair) = S (fst pair) , step (fst pair) (snd pair)

    iterate : (n : Nat) -> Σ Nat (\n -> P n)
    iterate Z = myalgebra None
    iterate (S n) = myalgebra (Some (iterate n))

    itlemma : (n : Nat) -> Id (fst (iterate n)) n
    itlemma Z     = Refl
    itlemma (S n) = resp S (itlemma n)

    ind : (n : Nat) -> P n
    ind n = subst P (itlemma n) (snd (iterate n))


  module Unique where

    natrec : (P : Nat -> Set) (base : (P Z)) (step : ((n : Nat) -> P n -> P (S n))) 
           -> (n : Nat) -> P n
    natrec P base step Z = base
    natrec P base step (S n) = step n (natrec P base step n)

    unique : (P : Nat -> Set) (base : (P Z)) (step : ((n : Nat) -> P n -> P (S n))) 
             (f : (n : Nat) -> P n)
             (id0 : Id (f Z) base) 
             (id1 : (n : Nat) -> Id (f (S n)) (step n (f n)))
             (n : Nat) -> Id (f n) (natrec P base step n)
    unique P base step f id0 id1 Z = id0
    unique P base step f id0 id1 (S n) =  trans (id1 n) (resp (\ x -> step n x) (unique P base step f id0 id1 n))