[Agda] Agda's coinduction incompatible with initial algebras

[Andreas Abel]

Nice.  You score!

However, I might critize the esthetics of your goal a bit.  You define a 
type Mu-co which is both inductive (via sizes) and coinductive (via co). 
  Then you show that it is both empty (via iter) and inhabited (via 
bla).  So far, quite beautiful.

But your type Mu-co could easily be ruled out by checking that a sized 
inductive type has no coinductive constructor fields.

Cheers,
Andreas

On 04.10.11 1:09 PM, Nicolas Pouillard wrote:
> -- npouillard, 2011-10-04
> {-# OPTIONS --sized-types #-}
> module False-coAlg-np where
>
> open import Coinduction renaming (∞ to co)
> open import Size
> data ⊥ : Set where
>
> data Mu-co : Size → Set where
>    inn : ∀ {i} → co (Mu-co i) → Mu-co (↑ i)
>
> iter : ∀ {i} → Mu-co i → ⊥
> iter (inn t) = iter (♭ t)
>
> bla : Mu-co ∞
> bla = inn (♯ bla)
>
> false : ⊥
> false = iter bla

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/