{-# OPTIONS --safe #-}

module Cubical.Induction.WellFounded where

open import Cubical.Foundations.Prelude

module _ { ℓ'} {A : Type } (_<_ : A  A  Type ℓ') where
  WFRec : ∀{ℓ''}  (A  Type ℓ'')  A  Type _
  WFRec P x =  y  y < x  P y

  data Acc (x : A) : Type (ℓ-max  ℓ') where
    acc : WFRec Acc x  Acc x

  WellFounded : Type _
  WellFounded =  x  Acc x


module _ { ℓ'} {A : Type } {_<_ : A  A  Type ℓ'} where
  isPropAcc :  x  isProp (Acc _<_ x)
  isPropAcc x (acc p) (acc q)
    = λ i  acc  y y<x  isPropAcc y (p y y<x) (q y y<x) i)

  isPropWellFounded : isProp (WellFounded _<_)
  isPropWellFounded p q i a = isPropAcc a (p a) (q a) i

  access : ∀{x}  Acc _<_ x  WFRec _<_ (Acc _<_) x
  access (acc r) = r

  private
    wfi : ∀{ℓ''} {P : A  Type ℓ''}
          x  (wf : Acc _<_ x)
         (∀ x  (∀ y  y < x  P y)  P x)
         P x
    wfi x (acc p) e = e x λ y y<x  wfi y (p y y<x) e

  module WFI (wf : WellFounded _<_) where
    module _ {ℓ''} {P : A  Type ℓ''} (e :  x  (∀ y  y < x  P y)  P x) where
      private
        wfi-compute :  x ax  wfi x ax e  e x  y _  wfi y (wf y) e)
        wfi-compute x (acc p)
          = λ i  e x  y y<x  wfi y (isPropAcc y (p y y<x) (wf y) i) e)

      induction :   x  P x
      induction x = wfi x (wf x) e

      induction-compute :  x  induction x  (e x λ y _  induction y)
      induction-compute x = wfi-compute x (wf x)