module SizedTypes where

open import Size
open import Coalgebras using (ListF; nil; cons; mapF)

-- Greatest fixed-points can be constructed by ordinal iteration.
-- Here, we follow deflationary iteration.

record Colist i A : Set where
  coinductive
  field force : ∀{j : Size< i} → ListF A (Colist j A)
open Colist

-- "Constructors" are defined via copattern matching.

[] : ∀{i A} → Colist (↑ i) A
force [] = nil

_∷_ : ∀{i A} → A → Colist i A → Colist (↑ i) A
force (a ∷ as) = cons a as

-- Coiteration, generically, productivity witnessed by sizes.

unfold : ∀{i A S} (t : S → ListF A S) → S → Colist i A
force (unfold t s) = mapF (unfold t) (t s)

-- Version with sizes made explicit.

e-unfold : ∀ i {A S} (t : S → ListF A S) → S → Colist i A
force (e-unfold i t s) {j} = mapF (e-unfold j t) (t s)