Lex total categories and Grothendieck toposes

This is the first of a series of connected posts. The next post is here.

In the very valuable volume Sketches of an Elephant, A Topos Theory Compendium, Volume 1, Peter Johnstone mentions a lecture of Andre Joyal at the 1981 Cambridge Summer Meeting where he listed seven different descriptions of 'what a topos is like'. His fifth one was

(v) 'A topos is a totally cocomplete object in the meta-2-category of  finitely complete categories'.

Read more »

The algebra of processes XI

Previous post in this series is here.

We have been thinking about categorical algebra for computer science now for 25 years. I want to discuss the problems of thinking seriously about two distinct disciplines, and how one might avoid the danger of falling between two stools.
Read more »

The seeds of homotopy type theory

I was recently very surprised to find a lecture (http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf) of Vladimir Voevodsky explaining his motivation for working on homotopy type theory and the mechanization of mathematics.

In brief the reason was that a group of well-known mathematicians working on "higher dimensional mathematics" since the 1980's were making errors which were not discovered for years, in one case not till more than 20 years after publication. Voevodsky refers to this situation as "outrageous".

Read more »