Rethinking Data and Codata Through Matrix Transposition

This paper formalizes de- and refunctionalization as matrix transposition between data and codata types in a dependently typed language. The authors prove that these transformations preserve typing, equality, and program well-formedness at the judgmental level. However, they identify open challenges around termination and productivity checking, universe hierarchies, variance restrictions, and behavioral equality—critical hurdles for extending the system into a consistent, fully fledged proof assistant.