Lazy Categories

Strict double categories are category objects in $\mathrm{𝐂𝐚𝐭}$, and much of their basic properties follow from the general theory of category objects, where the results are proved using standard, albeit complicated, limit arguments. When proving such results we secretly think that we are working with sets. Now, $\mathrm{𝐂𝐚𝐭}$ has many set-like properties but it is not $\mathrm{𝐒𝐞𝐭}$, so we shouldn’t be surprised when some things don’t work. For example profunctors don’t compose properly.

Instead of pretending that categories are sets, we turn this on its head and pretend that sets are categories. Well, not sets but the next best thing, the objects of a nice topos. Following Verity we embed $\mathrm{𝐂𝐚𝐭}$ in a topos which closely resembles it, whose objects we call lazy categories.

We investigate how much category theory carries over and what are the advantages of doing this.