------------------------------------------------------------------------
-- Andreas Abel and Brigitte Pientka,
-- Wellfounded Recursion with Copatterns and Sized Types.
--
-- Journal of Functional Programming, volume 26, 2016
--
-- Agda code for examples
------------------------------------------------------------------------

{-# OPTIONS --postfix-projections #-}

module FixedPointCombinators where

open import Prelude
open import Generic

------------------------------------------------------------------------
-- Section 2.7: Programming fixed-point combinators
------------------------------------------------------------------------

fixMu : ∀{i F} (A : Size → Set) →
  (∀{j} → ((k : Size< j) → Mu k F → A k) → Mu j F → A j) → Mu i F → A i
fixMu A f (inn t) = f (λ{ k → fixMu A f }) (inn t)

fixNu : ∀{i F} (A : Size → Set) →
  (∀{j} → ((k : Size< j) → A k → Nu k F) → A j → Nu j F) → A i → Nu i F
fixNu A f a .out = f (λ{ k → fixNu A f }) a .out