HoTT Math Series

I am planning to do a series of posts where I attempt to do math in Homotopy Type Theory (HoTT). The plan is to do some relatively simple proof-relevant mathematics at an informal level. The topics will all be undergraduate level so the mathematics won’t be hard to follow. I’m hoping to keep the series brief so each post will only be an appetizer and not a full course dinner. Enjoy!

This preamble will serve to accumulate a table of contents and various conventions and notations that come up along the way. The only prerequisites (or rather corequisites) are the first two chapters of the (free) Homotopy Type Theory book. Further prerequisites and reverences to later topics in the book will always be indicated where they occur.


  1. Elementary group theory
  2. More on equational logic
  3. Unit group of a ring
  4. Local rings and fields
 

Selected Papers Network

I just made my first contribution to the Selected Papers Network. It was fun and easy and I strongly recommend you use it too!

It’s too early for serious commentary on the experience but there are a few things I noted right away:

  • The front page selectedpapers.net does not yet support MathJax. (Neither does Google+ but that’s another problem.) Hopefully that will be fixed soon. Meanwhile, you can use the MathJax bookmarklet.
  • The hashtag syntax is fairly simple and intuitive but there is room for improvement. The main improvement would be to relax the ID rules to allow full urls which are easier to cut and paste. For example, http://arxiv.org/abs/1234.6789 for arXiv:1234.6789, http://dx.doi.org/10.1234/0987654321 for doi:10.1234/0987654321.
  • Comments do not seem to generate arXiv trackbacks. (Or they have not yet made it through the arXiv editorial process.)
  • I wish topic (hash)tags were allowed to have natural syntax. I can’t think of a good reason why this has to follow the Twitter standard. Should it be #cstarAlgebras or #CstarAlgebras or #CStarAlgebras… why not C*-algebras? It’s better to allow natural syntax and implement a tag synonym system.

You can track these and other issues here.

 

SMBC on madness…

It’s very easy to imagine a mad scientist: combine a bad hair day with a lab coat, surround with vats, oscillators, and other instruments, throw the mix into a cave and voilà!

It’s much harder to imagine a mad mathematician: bad hair and … what? Fortunately, SMBC has figured it out!
… 

 

Convergence of ideas

As a moderator on MathOverflow, I see a lot of interesting interactions between mathematicians. The occasional dramatic situations get discussed profusely by community but very few take the time talk about the pleasant exchanges they have had. Here is one that caught my attention today because it illustrates how it is not uncommon for two mathematicians from distant parts of the world can stumble upon the exact same set of ideas…

Today, Sean Eberhard asked two interesting questions: Intersecting group orbits and Intersecting group orbits, version 2. The first question was answered almost immediately by Andreas Blass with a carefully crafted argument. This is not unusual, Andreas is well-known for answering questions quickly and precisely, both on and off MathOverflow. However, Andreas’s comment after answering explains why he answered so fast:

This, along with the projective plane example, was actually going to be in a paper I’m writing. Fortunately, the main topic of the paper is something else, so the paper won’t lose much by omitting this.

After getting an answer from Andreas, Sean posted his second question. Andreas answered again, with another comment:

This is another piece of the planned paper that I mentioned in connection with Sean’s previous question. Maybe the whole paper will gradually appear on MO this way. It’s one way to get it written without my usual delays.

It appears that Sean and Andreas have been having a lot of common questions and ideas, even if they don’t appear to know each other and live on different continents. Let me conclude this anecdote by seconding one of Sean’s comments:

I look forward to reading this paper. 🙂

 

Disqus

I have just enabled Disqus commenting system. It has lots of nice features, but there are a few bugs we need to fix — that’s part of the Boole’s Rings way…

The most obvious issue is that MathJax currently doesn’t work in comments. I’m hoping that will get fixed very soon, so keep on using $\LaTeX$ in comments even if it’s not pretty for the moment.

There are a few other minor issues. Let me know if you encounter an issue, that will help us tune this new plugin.

 

Why write papers?

Here is what Dror Bar-Natan had to say about that on MathOverflow:

Papers are written so that their author(s) can forget their content and move on to other things. Therefore when you write you should be very careful to put in enough of the big picture and enough of the details so you’d be able to reconstruct your thoughts 10 years later if you’ll need to, assuming you’ll forget everything but retain some familiarity with some basic principles of mathematics.

It’s nice to think that papers could be so useful in light of the recent publishing debate