------------------------------------------------------------------------
-- 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 Generic where

open import Prelude

------------------------------------------------------------------------------
-- Section 2.4: Inflationary least and deflationary greatest fixed-point types
------------------------------------------------------------------------------

{-# NO_POSITIVITY_CHECK #-}
data Mu (i : Size) (F : Set → Set) : Set where
  inn : ∀{j : Size< i} → F (Mu j F) → Mu i F

{-# NO_POSITIVITY_CHECK #-}
record Nu (i : Size) (F : Set → Set) : Set where
  coinductive
  field out : ∀{j : Size< i} → F (Nu j F)
open Nu public

inMu : ∀{F i} → (∃ j < i , F (Mu j F)) → Mu i F
inMu (^ t) = inn t

inMu∞ : ∀{F} → F (Mu ∞ F) → Mu ∞ F
inMu∞ t = inn t

outNu : ∀{F i} → Nu i F → ∀{j : Size< i} → F (Nu j F)
outNu r = out r

outNu∞ : ∀{F} → Nu ∞ F → F (Nu ∞ F)
outNu∞ r = out r

outMu : ∀{F i} → Mu i F → ∃ j < i , F (Mu j F)
outMu (inn t) = ^ t

inNu : ∀{F i} → (∀{j : Size< i} → F (Nu j F)) → Nu i F
inNu t .out = t