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)