-- §──────────────────────────────────────────────────────────────────
-- This module was written only to help me understand well-foundedness
-- and recursion.
-- §──────────────────────────────────────────────────────────────────

-- §──────────────────────────────────────────────────────────────────
-- Modules required to specify the parameters of this module.
-- §──────────────────────────────────────────────────────────────────

import Level as L
import Relation.Binary as RB

-- §──────────────────────────────────────────────────────────────────
-- This module
-- §──────────────────────────────────────────────────────────────────

module My.SetTheory.Induction.WellFounded {𝓁 𝓂 : L.Level} {A : Set 𝓁}
  (_<_ : RB.Rel A 𝓂) where

-- §──────────────────────────────────────────────────────────────────
-- Other required modules
-- §──────────────────────────────────────────────────────────────────

import Relation.Unary as RU

open L using (_⊔_)

-- §──────────────────────────────────────────────────────────────────
-- Accesibility.  HoTT book, 10.3.1.
-- §──────────────────────────────────────────────────────────────────

data Acc (a : A) : Set (𝓁  𝓂)
  where
    acc : ((b : A)  b < a  Acc b)  Acc a

-- §──────────────────────────────────────────────────────────────────
-- Well-founded relation.  HoTT book, 10.3.3.
-- §──────────────────────────────────────────────────────────────────

WellFounded : Set (𝓁  𝓂)
WellFounded = (a : A)  Acc a

-- §──────────────────────────────────────────────────────────────────
-- Well-founded induction.  HoTT book, p.445.
-- §──────────────────────────────────────────────────────────────────

accRec : {𝓃 : L.Level}  (P : RU.Pred A 𝓃) 
  ((a : A)  ((b : A)  b < a  P b)  P a)  (a : A)  Acc a  P a
accRec P ihyp a (acc φ) = ihyp a ψ
  where
    ψ : (b : A)  (b<a : b < a)  P b
    ψ b b<a = accRec P ihyp b (φ b b<a)

wfRec : {𝓃 : L.Level}  (wf : WellFounded)  (P : RU.Pred A 𝓃) 
  ((a : A)  ((b : A)  b < a  P b)  P a)  (a : A)  P a
wfRec wf P ihyp a = accRec P ihyp a (wf a)