[Agda] Agda's coinduction incompatible with initial algebras

[Nils Anders Danielsson]

On 2011-10-06 15:10, Thorsten Altenkirch wrote:
> How do sized types interact with induction recursion?
> wiith induction-induction?
> And mixed induction/coinduction ?

I have played around with mixed induction/coinduction in MiniAgda, and
as far as I recall this worked fine (except for some overhead due to the
absence of ∞ and the need to juggle size indices).

Example:

   -- The partiality monad.

   sized codata Lift (+ A : Set) : Size -> Set
   { now   : [i : Size] -> A        -> Lift A ($ i)
   ; later : [i : Size] -> Lift A i -> Lift A ($ i)
   }

   -- The inductive part of weak bisimilarity.

   data Rel' (A : Set) (+ Rel : Lift A # -> Lift A # -> Set)
             (+ rel : A -> A -> Set) :
             Lift A # -> Lift A # -> Set
   { nowCong   : (v1, v2 : A) -> rel v1 v2 ->
                 Rel' A Rel rel (now A # v1) (now A # v2)
   ; laterCong : [x1, x2 : Lift A #] ->
                 Rel x1 x2 ->
                 Rel' A Rel rel (later A # x1) (later A # x2)
   ; laterL    : [x1, x2 : Lift A #] ->
                 Rel' A Rel rel x1 x2 ->
                 Rel' A Rel rel (later A # x1) x2
   ; laterR    : [x1, x2 : Lift A #] ->
                 Rel' A Rel rel x1 x2 ->
                 Rel' A Rel rel x1 (later A # x2)
   }

   -- Weak bisimilarity.

   sized codata Rel (A : Set) (+ rel : -Size -> A -> A -> Set) :
                    Size -> Lift A # -> Lift A # -> Set
   { tie : [i : Size] -> [x1, x2 : Lift A #] ->
           Rel' A (Rel A rel i) (rel ($ i)) x1 x2 ->
           Rel A rel ($ i) x1 x2
   }

-- 
/NAD