View Item 
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        JavaScript is disabled for your browser. Some features of this site may not work without it.

        Browse

        All of UU Student Theses RepositoryBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

        The Functorial Nature of Enriched Data Types

        Thumbnail
        View/Open
        thesis Lukas Mulder.pdf (912.4Kb)
        Publication date
        2024
        Author
        Mulder, Lukas
        Metadata
        Show full item record
        Summary
        In computer science, many popular data types can be modeled in a categorical framework. More specif- ically, they can be modeled as an initial algebra in the category of F-algebras for some endofunctor F : C → C. Examples include the booleans, the natural numbers, lists, trees and more generally al- gebraic data types, W -types and inductive data types. These initial algebras have the special property that algebra morphisms out of it to any other algebra always exist and are unique. This gives us tools to easily reason about functions defined on these data types. The downside to this approach is that we lose a lot of flexibly when defining maps, since they must respect the algebra structures completely. In a recent paper it has been shown that the category of F -algebras is enriched over the category of F-coalgebras, if the category C and functor F involved are sufficiently well-behaved. This gave a structured way to define so called measurings, which respect the algebra structure up to a certain point, granting more flexibility when defining morphisms. They also introduced the notion of a C-initial algebra for some F-coalgebra C, which shares the desirable properties of an initial algebra while accommodating the idea of a measuring. So far, the above has been applied to the example of natural numbers. First off, we will consider more examples, including the previously mentioned booleans, lists and trees. We will also expand on the existing theory, showing the construction of the enriched category of F -algebras is functorial in F . That is, given a natural transformation µ : F → G, we will construct enriched functors from the category of F-algebras to the category of G-algebras and vice versa. This gives rise to functors Endo(C) → EnrCat, where Endo(C) is the category of (sufficiently well-behaved) endomorphisms on C and natural transformations. The category EnrCat is the category of enriched categories and enriched functors, and will be defined in this thesis. Throughout the thesis, we will continue to pay attention to C-initial algebras, providing many examples and showing in which cases they are preserved between categories of algebras.
        URI
        https://studenttheses.uu.nl/handle/20.500.12932/47250
        Collections
        • Theses
        Utrecht university logo