# Representing Continuous Functions between Greatest Fixed Points of Indexed Containers

## TL;DR

This paper introduces a method to represent computable functions between coinductive types as transducers within type theory, extending previous work on streams to more complex coinductive structures, and formalizes these in Agda.

## Contribution

It generalizes earlier models of functions between streams to a broader class of coinductive types using dependent type theory and inductive-recursive definitions.

## Key findings

- Transducers can be defined without equality notions in dependent type theory.
- Most properties rely on a mild notion of equality, enabling formalization in Agda.
- The approach applies to a richer class of coinductive types beyond streams.

## Abstract

We describe a way to represent computable functions between coinductive types as particular transducers in type theory. This generalizes earlier work on functions between streams by P. Hancock to a much richer class of coinductive types. Those transducers can be defined in dependent type theory without any notion of equality but require inductive-recursive definitions. Most of the properties of these constructions only rely on a mild notion of equality (intensional equality) and can thus be formalized in the dependently typed language Agda.