Category theory is a branch of abstract mathematics that aims to give a high-level overview of relations between objects. Proof assistants are tools that aid in verifying the correctness of mathematical proofs. To reason about category theory using such assistants, fundamental notions have to be defined. Computer-checked libraries contain all relevant structures and theorems in an accessible way for end users. However, current libraries of category theory are not welcoming to people without in-depth domain knowledge. This paper introduces a library of category theory tailored towards newcomers to the field as well as the learning journey of the authors. We describe the project’s structure, design choices and provide examples of the main features. Moreover, a detailed overview is provided of F-algebras and their relation with inductive data types found in functional programming languages. Construction and evaluation of types like lists and binary trees can be defined in terms of algebras. They provide a general framework for recursion over these types which allow us to reason about them with simple functions.