## Dependent types overview

Proving things in Agda, part 1: what is dependent typing?

Proving things in Agda, part 1: what is dependent typing?

This is just a link to a beautiful proof of the Cauchy-Schwarz inequality. There are a number of elegant proofs, but this is by far my favourite, because (as...

Martin was walking through the farmers’ market. He had scored off nearly everything on his shopping list, but one item stubbornly remained: he needed some ka...

TL;DR: Being a beginner at something is great, especially if it’s something that humans are built for.

Now that my time in Part III is over, I feel justified in releasing my essay, which is on the subject of Non-standard Analysis. It was supervised by Dr Thoma...

I was recently having a late-night argument with someone about the following thesis:

There is a Hacker News thread at the moment about an article on Quanta which describes a paper which claims to prove that Ramsey’s theorem for pairs is finit...

Most recent exposition: an article on Tennenbaum’s Theorem. Comments welcome. The proof is cribbed from Dr Thomas Forster, but his notes only sketched the fa...

I’ve written a blurb about what a modular machine is (namely, another Turing-equivalent form of computing machine), and how a Turing machine may be simulated...

So you’ve heard that the Axiom of Choice is magical and special and unprovable and independent of set theory, and you’re here to work out what that means. Le...

Recall the Monty Hall problem: the host, Monty Hall, shows you three doors: A, B and C. You are assured that behind one of the doors is a car, and behind the...

I’ve been trying to learn Clojure (a LISP) through Exercism, a programming exercises tool. It took me an hour to get Hello, World! up and running, so I thoug...

This post is incomplete.

Another short post to point out my new article on the Friedberg-Muchnik theorem, a theorem from computability theory. It uses what is known officially as a f...

Just a post to draw attention to my new article about representable functors and their links to adjoint functors. It’s very short, but it gives a reason for ...

I’m clearing out my desktop again, and found this document on the multiplicativity of the determinant, which I wrote in 2014. It might as well be up here.

Another short post to highlight the existence of an article about the Monadicity Theorems, in which I prove one direction of both the Crude and Precise versi...

Just a post to draw attention to my new article about the General Adjoint Functor Theorem. It’s a motivation of the GAFT and its proof. I’ve never seen it mo...

In the Part III Topics in Set Theory course, we have used forcing to show the consistency of the Continuum Hypothesis, and we are about to show the consisten...

During my attempts to understand the fearsomely difficult Part III course “Introduction to Category Theory” by PT Johnstone, I came across the monadicity of ...

Now that we’ve had the definition of an exponential, we move on to the Heyting algebra, pages 129 through 131 of Awodey. This is still in the “exponentials” ...

These are located on pages 114 through 118 of Awodey.

Now we come to Chapter 6 of Awodey, on exponentials, pages 119 through 128. Supposedly, this represents a kind of universal property which is not of the form...

It has been proposed to me that if one is to play the National Lottery, one should be sure to select one’s own numbers instead of allowing the machine to sel...

We’ve seen how limits are formed, and that they exist iff products and equalisers do. Now we get to see about continuous functions and colimits, pages 105 th...

We have just had the definition of a pullback; now in Awodey pages 95 through 100 we’ll see some more about them, and after that we’ll get the more general u...

I’m going to skip pages 85 through 88 of Awodey for the moment, because time is starting to get short and I want to make sure I’m doing stuff which is releva...

I go into this chapter hoping that it will be on things I already know about group theory. This post will be on pages 75 through 85 of Awodey.

Exercise 1 is easy: at the end of Chapter 2 the corresponding products statement was proved, and the obvious dual statement turns out to be this one.

This is pages 62 through 71 of Awodey, on equalisers and coequalisers.

I don’t have strong preconceptions about this chapter. The previous chapter I knew would contain general constructions, and I was looking forwards to that, b...

This is on pages 48 through 52 of Awodey, covering the hom-sets section and the exercises at the end of Chapter 2. Only eight more chapters after this, and I...

This is on pages 38 through 48 of Awodey. I’ve been looking forward to it, because products are things which come up all over the place and I’d heard that th...

This is pages 33 to 38 of Awodey.

This post is on pages 29 through 33 of Awodey. It took me a while to do this, because I was basically on holiday for the past week.

Here I explain proof by contradiction so that anyone who has ever done a sudoku and seen algebra may understand it.

Here, I will be going through the Free Categories and Foundations sections of Awodey’s Category Theory - pages 18 through 25.

Here, I will be going through the Isomorphisms and Constructions sections of Awodey’s Category Theory - pages 12 through 17.

This post will cover the initial “examples” section of Category Theory. Because there aren’t really very deep concepts in this section, this is probably a le...

The next few posts will be following me on my journey through the book Category Theory, by Steve Awodey. I’m using the second edition, if anyone wants to joi...

In which I am a wizard.

I’m clearing out my computer, and found a file which may as well be here.

I recently saw a problem from an Indian maths olympiad:

I’ve just come back from seeing Interstellar, a film of peril and physics. This post will be spoiler-free except for sections which are in rot13.

In which I provide my favourite carols and my favourite renditions of them.

Wherein I detail the most beautiful proof of a theorem I’ve ever seen, in a bite-size form suitable for an Anki deck. I attach the Anki deck, which contains ...

A very brief post about the solution to a problem I came across in Python.

One day, a group of investors came to Bezos in the Temple and begged of him, “You are known throughout the land for your wisdom. Please tell us: what lessons...

I have a limited form of perfect (absolute) pitch, which I am sometimes asked about. Often it’s the same questions, so here they are. No doubt people with be...

A couple of weeks ago, someone opined to me that there was a type of person who was just able to sit down and play at the piano, without sheet music.

In my activities on The Student Room, a student forum, someone (let’s call em Entity, because I like that word) recently asked me about the following questio...

Recently, a friend re-introduced me to the joys of the nonogram (variously known as “hanjie” or “griddler”). I was first shown these about ten years ago, I t...

I have seen many glowing reviews of Soylent, and many vitriolic naturalistic arguments against it. What I have not really seen is a proper collection of cred...

This comes up quite frequently, but I’ve been stuck for an easy memory-friendly way to do this. I trawled through the 1A Vectors and Matrices course notes, a...

This is part of what has become a series on discovering some fairly basic mathematical results, and/or discovering their proofs. It’s mostly intended so that...

Prof Körner told us during the IB Metric and Topological Spaces course that the real meat of the course (indeed, its hardest theorem) was “a metric space is ...

This is to detail a much easier proof (at least, I find it so) of Cayley-Hamilton than the ones which appear on the Wikipedia page. It only applies in the ca...

As part of the recent series on how I approach maths problems, I give another one here (question 14 on the Maths Tripos IB 2007 paper 4). The question is:

This post is to be a list of conformal mappings, so that I can get better at answering questions like “Find a conformal mapping from <this domain> to &...

I’m running through my Analysis proofs, trying to work out which ones are genuinely hard and which follow straightforwardly from my general knowledge base. I...

A little while ago I set myself the exercise of stating and proving the Contraction Mapping Theorem. It turned out that I mis-stated it in three different as...

It has been commented to me that it’s quite hard to find out (on the Internet) what different games involve. For instance, Agricola is a game about farming (...

I feel that I can write a sonnet well. While sonnets are an easy thing to spout, It’s really hard to write a villanelle.

The aim of this post is twofold: to find out whether a certain mental habit of mine is common, and to draw parallels between that habit and the writing of es...

Recently, I was browsing the Wolfram Community forum, and I came across the following question:

A long time ago, in a galaxy far far away, I completed Myst III: Exile. It’s a stupendously good puzzle game. For some reason, it popped into my mind again a...

Once upon a time, before this bountiful age of Matter and Light, there was only the Fell. A single being, surrounded by Chaos, content to remain alone foreve...

I am shortly to receive a new Nexus 5. I am determined not to become a smartphone zombie, and so I hereby commit to the following Charter.

Earlier today, I had a rather depressing conversation with several people, in which it was revealed to me that many people will attempt to argue against the ...

The book Don’t Shoot the Dog, by Karen Pryor, contains a simple exercise in demonstrating clicker training. This is a very successful technique used to produ...

Many thanks to the Guru Bursill-Hall for bringing this tract to my attention through his weekly History of Maths bulletins. It was originally written in 1...

In my latest lecture on Markov Chains in Part IB of the Mathematical Tripos, our lecturer showed us a very nice little application of the theorem that “if a ...

*This post is unfinished, and may never be finished - I have decided that the Nexus 5 is sufficiently cheap, nice-looking and future-proof to outweigh the bo...

This post is for posterity, made shortly after Dr Paul Russell lectured Analysis II in Part IB of the Maths Tripos at Cambridge. In particular, he demonstrat...

Once upon a midnight dreary, while I pondered, weak and weary, I required a snack to feed me. Reaching in the kitchen drawer - With the scissors, cut the wra...

In which I recount an experiment I have been performing. Please be aware that in this article I am in “meaning what I say” mode.

In conversation with (say, for the purposes of propagating a sterotype) humanities students, I am often struck by how imprecisely language is used, and how m...

Wherein I dabble in parodic fiction. The title refers to the TV Tropes page on Plot Armour, but don’t follow that link unless you first resolve not to click ...

I came across an interesting question while reading the blog of Scott Aaronson today. The question was as follows:

On the merits of silence (I wholeheartedly agree): http://www.nytimes.com/2013/08/25/opinion/sunday/im-thinking-please-be-quiet.html

This is a collection of poems which together prove the Sylow theorems.

I’ve been learning some basic topology over the last couple of months, and it strikes me that there are some very confusing names for things. Here I present ...

The much-vaunted Hyperloop looks really cool, if it could ever be built: http://arstechnica.com/business/2013/08/hyperloop-a-theoretical-760-mph-transit-s...

When in Cambridge…

I’m in the middle of reading Flow, by Mihály Csíkszentmihályi, and so far, I love it. It describes the “flow state” of consciousness, that state of “everythi...

All the way back into primary school (ages 4 to 11 years old, in case a non-Brit is reading this), we have been told repeatedly that “people learn things in ...

A thousand times this: http://www.webcitation.org/6IdkckgOX A possible fix for the “economic problem of democracy”: http://hanson.gmu.edu/futarchy.html ...

An ad developer has misgivings: http://seriouspony.com/blog/2013/7/24/your-app-makes-me-fat Hint for dealing with some automated phone helplines - swear...

In case I ever have to get a new computer (or, indeed, in case anyone else is interested), I hereby present the (updating) list of applications and so forth ...

Getting Things Done has gathered something of a cult following [archived due to link rot] since its inception. As a way of getting things done, it’s pretty g...

Hehe: http://www.pixartheory.com/ Wow - light trapped for a full minute: http://www.newscientist.com/article/dn23925-light-completely-stopped-for-a-reco...

I have recently discovered the game of Agricola, a board game involving using resources (family members, stone, etc) to build a thriving farm. The game is tu...

This is something I will try at some point, probably when I get back to uni: http://www.bulletproofexec.com/how-to-make-your-coffee-bulletproof-and-your-m...

The Orbit/Stabiliser Theorem is a simple theorem in group theory. Thanks to Tim Gowers for the proof I outline here - I find it much more intuitive than the ...

I’ve now seen two Shakespeare plays at the Globe - once in person, to see A Midsummer Night’s Dream, and once with a one-year-and-eighty-mile gap between vie...

A large chunk of the reason why changing someone’s mind is so difficult is the fact that our deeply-held beliefs seem so obviously true to us, and we find it...

I’ve been reading one of Daniel Dennett’s books, Consciousness Explained. Aside from the fact that the author has an incredible beard and is therefore correc...

Usually when I discover (or, more rarely, think up) a thought experiment about a moral point, and discuss it with an arbitrary person whom I will (for conven...

This is really quite heartwarming: http://www.reddit.com/r/Random_Acts_Of_Pizza/ Interesting article on current trends in fiction: http://www.locusmag.c...

Sometimes some people argue that certain things are “priceless” - that is, worth an infinite amount of money to them. I posit that what this really means is ...

There was once a small website devoted to noting the more interesting quotes from our more idiosyncratic lecturers. It has sadly vanished from the web - alth...

Being bored over the summer holiday, I decided that I would document the cool things I ran across on the Internet. Over the last week, there have been many o...

So yesterday the Wimbledon tennis tournament was decided. The system for verifying whether the tennis ball is out or not (and hence whether play for the poin...

I have stumbled across a LessWrong post on the importance of seeing what is real for just how cool it is. It lists such examples as:

There is an awfully large collection of confusing words you will encounter on first coming to study at Cambridge. You pick them up really quickly in the natu...

I wrote this when I was excessively bored during exam term of my first year. It may grow as I get better at working (I’m something of a revisionist). The adv...

(This is my first post written in Dvorak; accordingly, it is a bit shorter than I would like, since I am very slow at it. Tsuyoku naritai, and all that.)

(This post is mostly to set up a kind of structure for the website; in particular, to be the first in a series of posts summarising some mathematical results...

Hello all!

At the end of last (that is, Lent 2012-2013) term at Cambridge, I took part in the Cambridge University Computing and Technology Society Puzzlehunt (for some...