This work primarily stems from a personal journey of peering deeper into pure mathematics. The journey started as a curiosity into the functional programming paradigm, initially involving learning scala and basic PL theory such as generics, parametric polymorphism and the likes. Being a data engineer at that time, twitter’s work on designing metrics as monoids culminating in Algebird was something that had a lasting impression on my own work. This led me to explore libraries implementing bits of category theory such as shapeless cats, Algebird’s hyperloglog monoid, scalaz followed by several “for programmer” tutorials into category theory, notably the ones by Bartosz Milewski.Soon I had to learn haskell − it being more “pure” and having a stronger ecosystem of libraries with a more formal programming-language-theory flavor so as to have more things in this space to explore.

In tandem, I picked up a few books on the subjects of abstract algebra and category theory to get a theoretical understanding of the “whole thing”:

- Category Theory for Programmers ~ Milewski (repo)
- Abstract Algebra ~ Dummit & Foote (link)
- Topoi - The Categorical Analysis of Logic ~ Goldblatt (link)
- Categories for the Working Mathematician ~ Mac Lane (link)
- Algebra ~ Lang (link)

After that I turned toward some PL-theory:

- Practical Foundations for Programming Languages ~ Harper (link)
- An Introduction to Functional Programming Through Lambda Calculus - Michaelson (pdf)
- Robert Harper’s lectures on:

Followed by some “time off” into other areas of math:

- An Introduction to Manifolds ~ Tu (link)
- A Comprehensive Introduction to Differential Geometry Volume I ~ Spivak (link)
- A Concise Course in Algebraic Topology ~ May (pdf)

The “time off” ended upon discovering this new “foundations of mathematics” thing seen of twitter, materialized into 2 copies ordered from different sources, one of them never got delivered:

- Homotopy Type Theory ~ Univalent Foundations of Mathematics (link)

As things started getting more cutting-edge, it has mostly been a paper and articles reading affair since then. Major ones being:

Of late, I stumbled upon this work on mathematical physics:

- Gauge fields, knots, and gravity ~ Baez (link)
- Susskind’s lectures on:

opening the path to these shiny new thingys that await:

- geometry of physics (link)
- Differential cohomology in a cohesive ∞-topos ~ Schreiber (link)
- Quantum Gauge Field Theory in Cohesive Homotopy Type Theory ~ Schreiber (pdf)

It has been almost 4 years now, and the “whole thing” does not seem to have an end!

This work is intended to be a resource for anyone (like me) making a foray into pure mathematics. The “like me” here implies someone who:

- knows programming.
- has worked with functional programming in some capacity.
- has at least a sketchy idea of what “pure mathematics” means.
- has boundless motivation to explore.

Agda is a dependently-typed functional programming language that can be used as a “proof assistant” of the “propositions-as-types” flavor, i.e. it is a language used to write mathematical proofs, using a typesystem, which its compiler then verifies to check if the proofs really do what they claim. This is done by using Type theory as the language for writing proofs in Agda. Traditionally, the act of checking the validity of a proof has been a manual and painstaking process, however, the proofs when represented in this `code ⇆ compiler`

paradigm, does away with the need for manual checking, thus making things considerably easier to implement, test and distribute. There are other alternative theorem provers, each with their own feature-sets, strengths and weaknesses, documented here.

Agda was originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. The current version is a full rewrite, and should be considered a new language that shares a name and tradition.