Sciweavers

Share
ENTCS
2006

Continuous Functions on Final Coalgebras

8 years 8 months ago
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
Neil Ghani, Peter Hancock, Dirk Pattinson
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Neil Ghani, Peter Hancock, Dirk Pattinson
Comments (0)
books