Dependently-typed languages allow one to guarantee correctness of a program by providing formal proofs. The type checkers of such languages elaborate the user-friendly high-level surface language to a small and fully explicit core language. A lot of trust is put into this elaboration process, even though it is rarely verified. One such elaboration is elaborating dependent pattern matching to the low-level construction of eliminators. This elaboration is done in two steps. First, the function defined by dependent pattern matching is translated into a case tree, which can then be further translated to eliminators. We present a generic, well-typed implementation of this second step in Agda, without the use of metaprogramming and unsafe transformations, by providing a type-safe, correct-by construction, generic definition of case trees and an evaluation function that, given an interpretation of such a case tree and an interpretation of the telescope of function arguments, evaluates the output term of the function using only eliminators. We only allow case splits on variables from a fixed universe of data type descriptions, for which we use techniques like basic analysis and specialization by unification.

This research project aims to develop a computer-checked library of category theory within the Lean proof assistant, with a specific emphasis on concepts and examples relevant to functional programming. Category theory offers a robust mathematical framework that allows for the abstraction and comprehension of concepts across diverse fields, including computer science. Additionally, the project will explore the application of final coalgebras, particularly in the context of understanding infinite data structures. By creating a formalized category theory library within Lean, our objective is to enhance our understanding of functional programming and programming language concepts. Moreover, we aim to facilitate the study of these topics by providing a comprehensible library and a rigorous foundation for program reasoning, thereby benefiting researchers and practitioners in the field.