#+title: Category-Theory

This is an attempt at formalizing basic category theory in Agda by myself as practice to better understand both Agda and category theory.

My main category theory reference is /Category Theory/ by Steve Awodey (supplemented by MacLane and /Categories in Context/ by Emily Riehl).

My main reference for Agda is [[https://plfa.github.io/][Programming Languages Foundations in Agda]] and browsing [[https://agda.github.io/agda-stdlib/v2.1.1/][the standard library]].

Use [[https://github.com/agda/agda-categories][this excellent library]] for any real category theory work.