-- §──────────────────────────────────────────────────────────────────
-- 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)