[Agda] Agda's coinduction incompatible with initial algebras

[Nicolas Pouillard]

On Tue, Oct 4, 2011 at 12:26 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> I'd like to open a new round of false-golfing, below is my entry to the
> tournament.  My favorite target is Agda's coinduction mechanism. Partially
> it's flaws are known, but I cannot remember anyone presenting an outright
> proof of the absurdity.  So here it is.

Ok, my turn to golf it down (one flag less):

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

-- 
Nicolas Pouillard
http://nicolaspouillard.fr