Specifying Datastructures via Coinduction

Consider the specification of Queue: we've got the constructors of a list, but the destructors of a reversed list! In other words, it is an Algebra for $1+A\times(-)$, and a Coalgebra for $1+A\times(-)$ that's been "twisted" by the map rev : List A → Colist A.