Coalgebraic reasoning in Coq: bisimulation and lambda-coiteration scheme

In this work we present a modular theory of the coalgebras and bisimulation in the intensional type theory implemented in Coq. On top of that we build the theory of weakly final coalgebras and develop the lambda-coiteration scheme, thereby extending the class of specifications definable in Coq. We provide an instantiation of the theory for the coalgebra of streams and show how some of the productive specifications violating the guardedness condition of Coq can be formalised using our library.