Continuous Functions on Final Coalgebras

It can be traced back to Brouwer that continuous functions of type StrA B, where StrA is the type of infinite streams over elements of A, can be represented by well founded, Abranching trees whose leafs are elements of B. This paper generalises the above correspondence to functions defined on final coalgebras for power-series functors on the category of sets and functions. While our main technical contribution is the characterisation of all continuous functions, defined on a final coalgebra and taking values in a discrete space by means of inductive types, a methodological point is that these inductive types are most conveniently formulated in a framework of dependent type theory. Key words: Continuous Functions, Final Coalgebras, Constructive Mathematics

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Neil Ghani, Peter Hancock, Dirk Pattinson
• Keywords: Continuous Functions, ENTCS 2006, Final Coalgebras, Inductive Types