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.

@article{paperbot1293,
  title = {Representing Continuous Functions between Greatest Fixed Points of Indexed Containers},
  author = {Pierre Hyvernat},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 17, Issue 3},
  year = {2021},
  doi = {10.46298/lmcs-17(3:13)2021}
}