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