{-# OPTIONS --safe --cubical-compatible --erased-matches #-}
open import Equality
module Accessibility.Erased-matches
{e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where
open import Erased.Basics as Erased
open import Prelude
open import Accessibility eq
private variable
a p r : Level
well-founded-induction-Acc :
{@0 A : Type a} {@0 _<_ : A → A → Type r}
(@0 P : A → Type p) →
(∀ x → (∀ y → @0 y < x → P y) → P x) →
∀ x → @0 Acc _<_ x → P x
well-founded-induction-Acc P f x (acc g) =
f x (λ y y<x → well-founded-induction-Acc P f y (g y y<x))
well-founded-induction :
{@0 A : Type a} {@0 _<_ : A → A → Type r} →
@0 Well-founded _<_ →
(@0 P : A → Type p) →
(∀ x → (∀ y → @0 y < x → P y) → P x) →
∀ x → P x
well-founded-induction wf P f x =
well-founded-induction-Acc P f x (wf x)
Acc-erasure-stable :
{@0 A : Type a} {@0 _<_ : A → A → Type r} {@0 x : A} →
Erased.Stable (Acc _<_ x)
Acc-erasure-stable [ acc f ] =
acc (λ y y<x → Acc-erasure-stable [ f y y<x ])
Well-founded-erasure-stable :
{@0 A : Type a} {@0 _<_ : A → A → Type r} →
Erased.Stable (Well-founded _<_)
Well-founded-erasure-stable [ wf ] = λ x →
Acc-erasure-stable [ wf x ]