Acc

Accessibility.agda

module Accessibility where

data Acc {A : Set} (R : A → A → Set) (a : A) : Set where
  step : (∀ b → R b a → Acc R b) → Acc R a 

□^ : ∀ {A : Set} (R : A → A → Set) → (A → Set) → (A → Set)
□^ R P a = ∀ b → R b a → P b

[_] : {A : Set} → (A → Set) → Set
[ P ] = ∀ {a} → P a

infixr 5 _⟶_
_⟶_ : {A : Set} → (A → Set) → (A → Set) → (A → Set)
(P ⟶ Q) a = P a → Q a

fix : ∀ {A : Set} {R : A → A → Set} →
      [ Acc R ] → ∀ P → [ □^ R P ⟶ P ] → [ P ]
fix {A} {R} acc P f = go acc where

  go : [ Acc R ⟶ P ]
  go (step acc) = f (λ b Rba → go (acc b Rba))