▶ ANTON SETZER, Weakly final coalgebras in Martin-Löf type theory. Dept. of Computer Science, Swansea University, Singleton Park Swansea SA2 8PP, UK.

E-mail: a.g.setzer@swan.ac.uk.
URL Address: http://www.cs.swan.ac.uk/∼csetzer/.

Martin-Löf type theory (MLTT) is based on the dependent function type and (inductively defined) algebraic types. In order to model concepts like interaction or object-orientation in MLTT in a direct way, it is useful to add (coinductively defined) weakly final coalgebras to MLTT. We introduce formation, introduction, elimination, and equality rules for weakly final coalgebras in MLTT. We will show that guarded induction is nothing but an informal description of the introduction rules for weakly final coalgebras.

We investigate the duality between algebraic and coalgebraic types in those rules: For algebraic types the introduction rules are simple and predicative, the elimination rules involve some degree of impredicativity. There is a large variety of possible elimination rules, all of which are derived from the principle of having a least set closed under the introduction rules. For coalgebraic types, the elimination rules are simple and predicative, whereas the introduction rules involve some degree of impredicativity. There is a large variety of possible introduction rules, all of which are derived from the principle of having the largest set allowing the elimination principle.

We introduce a model of the extension of MLTT by weakly final coalgebras, and investigate the implications for meaning explanations, namely the need for types, the meaning of which is given by an elimination principle.

We will then show that bisimulation is an example of a dependent weakly final coalgebra. We demonstrate that proofs by guarded induction of bisimulation form a much more intuitive way of proving bisimulation properties than the usual proofs based on the introduction of a bisimulation relation.