Frontier algorithm

Frontier.agda

open import Agda.Primitive
open import Agda.Builtin.Equality

data Chain {n} {A : Set n} (f : A → A) (x : A) : A → Set (lsuc n) where
  nil  : Chain f x x
  link : ∀{y} → Chain f x y → Chain f x (f y)

record FixedPoint {n} {A : Set n} (R : A → A → Set) (f : A → A) : Set (lsuc n) where
  constructor fp
  field
    point : A
    fixed : R point (f point)
open FixedPoint public

record Limit {n} {A : Set n} (R : A → A → Set) (f : A → A) (x : A) : Set (lsuc n) where
  constructor limit
  field
    converges : FixedPoint R f
    attains   : Chain f x (point converges)
open Limit public