`module Lang.intro where`

The following work aims to be a primer and motivator for functional programmers to peer into the world of pure mathematics. This work is created by a functional programmer who, while discovering and using libraries and constructs like cats, scalaz, lens, monads and various other functional constructs built into languages such as haskell, scala, clojure, rust, purescript and so on, ended up with interest about the math behind them.

This work primarily stems from a personal journey of peering deeper into pure mathematics. The journey started in about 2014 partly as hatred toward the verbosity of java and as a curiosity into the functional programming paradigm made possible on the JVM through scala. Learning scala was soon followed by several PL treats such as generics, parametric polymorphism and the likes making my life easier. Being a data engineer at that time, twitter’s work on designing metrics as monoids and the Algebird project 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 accessible to explore.

In tandem, I started a parallel hobby-type thing where 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 trudging through some parts of the above books and getting a “feel” and practice of the mathematics in them, specifically category theory in various contexts, 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:

By 2018, I decided to converge some aspects of my programming job with the act of taking math notes. After I came to know of Agda’s capability to compile code in markdown docs (being a huge proponent of markdown for documentation), I decided to learn agda and concurrently document and code my exploration path into a series of notes, which ended up being this work.

One fine day, I saw this new “foundations of mathematics” thing, which apparently “cool kids” were reading on twitter. On further searching followed by reading online, I ended up ordering 2 copies from different sources, one of them never got delivered:

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

It took me a few months to read and grasp what was going on in that book. After spending considerable amounts of time through various other notes, mathoverflow, nlab, arxiv, I ended up with the feeling that I knew nothing about geometry and in no way could grasp homotopy theory. I took some time off in 2019 as these notes grew in volume and it became increasingly difficult to code them. During that time off I decided to cover some ground in geometry:

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

After going through these I finally was able to have at least a sketchy view of homotopy type theory, higher category theory and higher topos theory. As things started getting more cutting-edge, I’ve mostly ended up printing and reading through various parts of:

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)

Meanwhile I try to play catchup with this work and sometimes re-do some parts as my understanding gets clearer and sometimes implement new stuff as and when I have time (and patience). The direction I’ve been following here is if I could implement real numbers, followed by manifolds and such, I perhaps could attempt to implement gauge theories or Supermanifolds albeit it would take me a few years at least. I also need to finish a lot of TODOs. 😛

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.