Anafunctors

This is part four in a series of posts on avoiding the axiom of choice (part one, part two, part three).

In my previous post, we considered the “Axiom of Protoequivalence”—that is, the statement that every fully faithful, essentially surjective functor (i.e. every protoequivalence) is an equivalance—and I claimed that in a traditional setting this is equivalent to the axiom of choice. However, intuitively it feels like AP “ought to” be true, whereas AC must be rejected in constructive logic.

One way around this is by generalizing functors to anafunctors, which were introduced by Makkai (1996). The original paper is difficult going, since it is full of tons of detail, poorly typeset, and can only be downloaded as seven separate postscript files. There is also quite a lot of legitimate depth to the paper, which requires significant categorical sophistication (more than I possess) to fully understand. However, the basic ideas are not too hard to grok, and that’s what I will present here.

It’s important to note at the outset that anafunctors are much more than just a technical device enabling the Axiom of Protoequivalence. More generally, if everything in category theory is supposed to be done “up to isomorphism”, it is a bit suspect that functors have to be defined for objects on the nose. Anafunctors can be seen as a generalization of functors, where each object in the source category is sent not just to a single object, but to an entire isomorphism class of objects, without privileging any particular object in the class. In other words, anafunctors are functors whose “values are specified only up to unique isomorphism”.

Such functors represent a many-to-many relationship between objects of \mathbb{C} and objects of \mathbb{D}. Normal functors, as with any function, may of course map multiple objects of \mathbb{C} to the same object in \mathbb{D}. The novel aspect is the ability to have a single object of \mathbb{C} correspond to multiple objects of \mathbb{D}. The key idea is to add a class of “specifications” which mediate the relationship between objects in the source and target categories, in exactly the same way that a “junction table” must be added to support a many-to-many relationship in a database schema, as illustrated below:

On the left is a many-to-many relation between a set of shapes and a set of numbers. On the right, this relation has been mediated by a “junction table” containing a set of “specifications”—in this case, each specification is simply a pair of a shape and a number—together with two mappings (one-to-many relations) from the specifications to both of the original sets, such that a specification maps to a shape s and number n if and only if s and n were originally related.

In particular, an anafunctor F : \mathbb{C} \to \mathbb{D} is defined as follows.

  • There is a class S of specifications.
  • There are two functions \mathrm{Ob}\ \mathbb{C}  \stackrel{\overleftarrow{F}}{\longleftarrow} S  \stackrel{\overrightarrow{F}}{\longrightarrow} \mathrm{Ob}\ \mathbb{D} mapping specifications to objects of \mathbb{C} and \mathbb{D}.

S, \overleftarrow{F}, and \overrightarrow{F} together define a many-to-many relationship between objects of \mathbb{C} and objects of \mathbb{D}. D \in \mathbb{D} is called a specified value of F at C if there is some specification s \in S such that \overleftarrow{F}(s) = C and \overrightarrow{F}(s) = D, in which case we write F_s(C) = D. Moreover, D is a value of F at C (not necessarily a specified one) if there is some s for which D \cong F_s(C).

The idea now is to impose additional conditions which ensure that F “acts like” a regular functor \mathbb{C} \to \mathbb{D}.

  • Functors are defined on all objects; so we require each object of \mathbb{C} to have at least one specification s which corresponds to it—that is, \overleftarrow{F} must be surjective.
  • Functors transport morphisms as well as objects. For each s,t \in   S (the middle of the below diagram) and each f :   \overleftarrow{F}(s) \to \overleftarrow{F}(t) in \mathbb{C} (the left-hand side below), there must be a morphism F_{s,t}(f) :   \overrightarrow{F}(s) \to \overrightarrow{F}(t) in \mathbb{D} (the right-hand side):

  • Functors preserve identities: for each s \in S we should have F_{s,s}(\mathit{id}_{\overleftarrow{F}(s)}) = \mathit{id}_{\overrightarrow{F}(s)}.
  • Finally, functors preserve composition: for all s,t,u \in S (in the middle below), f : \overleftarrow{F}(s) \to \overleftarrow{F}(t), and g : \overleftarrow{F}(t) \to \overleftarrow{F}(u) (the left side below), it must be the case that F_{s,u}(f ; g) = F_{s,t}(f) ; F_{t,u}(g):

Our initial intuition was that an anafunctor should map objects of \mathbb{C} to isomorphism classes of objects in \mathbb{D}. This may not be immediately apparent from the definition, but is in fact the case. In particular, the identity morphism \mathit{id}_C maps to isomorphisms between specified values of C; that is, under the action of an anafunctor, an object C together with its identity morphism “blow up” into an isomorphism class (aka a clique). To see this, let s,t \in S be two different specifications corresponding to C, that is, \overleftarrow{F}(s) = \overleftarrow{F}(t) = C. Then by preservation of composition and identities, we have F_{s,t}(\mathit{id}_C) ; F_{t,s}(\mathit{id}_C) = F_{s,s}(\mathit{id}_C ; \mathit{id}_C) = F_{s,s}(\mathit{id}_C) = \mathit{id}_{\overrightarrow{F}(s)}, so F_{s,t}(\mathit{id}_C) and F_{t,s}(\mathit{id}_C) constitute an isomorphism between F_s(C) and F_t(C).

There is an alternative, equivalent definition of anafunctors, which is somewhat less intuitive but usually more convenient to work with: an anafunctor F : \mathbb{C} \to \mathbb{D} is a category of specifications \mathbb{S} together with a span of functors \mathbb{C} \stackrel{\overleftarrow{F}}{\longleftarrow} \mathbb{S} \stackrel{\overrightarrow{F}}{\longrightarrow} \mathbb{D} where \overleftarrow{F} is fully faithful and (strictly) surjective on objects.

Note that in this definition, \overleftarrow{F} must be strictly (as opposed to essentially) surjective on objects, that is, for every C \in \mathbb{C} there is some S \in \mathbb{S} such that \overleftarrow{F}(S) = C, rather than only requiring \overleftarrow{F}(S) \cong C. Given this strict surjectivity on objects, it is equivalent to require \overleftarrow F to be full, as in the definition above, or to be (strictly) surjective on the class of all morphisms.

We are punning on notation a bit here: in the original definition of anafunctor, S is a set and \overleftarrow{F} and \overrightarrow{F} are functions on objects, whereas in this more abstract definition \mathbb{S} is a category and \overleftarrow{F} and \overrightarrow{F} are functors. Of course, the two are closely related: given a span of functors \mathbb{C} \stackrel{\overleftarrow{F}}{\longleftarrow} \mathbb{S} \stackrel{\overrightarrow{F}}{\longrightarrow} \mathbb{D}, we may simply take the objects of \mathbb{S} as the class of specifications S, and the actions of the functors \overleftarrow{F} and \overrightarrow{F} on objects as the functions from specifications to objects of \mathbb{C} and \mathbb{D}. Conversely, given a class of specifications S and functions \overleftarrow{F} and \overrightarrow{F}, we may construct the category \mathbb{S} with \mathrm{Ob}\ \mathbb{S} = S and with morphisms \overleftarrow{F}(s) \to \overleftarrow{F}(t) in \mathbb{C} acting as morphisms s \to t in \mathbb{S}. From \mathbb{S} to \mathbb{C}, we construct the functor given by \overleftarrow{F} on objects and the identity on morphisms, and the other functor maps f : s \to t in \mathbb{S} to F_{s,t}(f) : \overrightarrow{F}(s) \to \overrightarrow{F}(t) in \mathbb{D}.

Every functor F : \mathbb{C} \to \mathbb{D} can be trivially turned into an anafunctor \mathbb{C} \stackrel{\mathit{Id}}{\longleftarrow} \mathbb{C} \stackrel{F}{\longrightarrow} \mathbb{D}. Anafunctors also compose. Given compatible anafunctors F : \mathbb{C} \stackrel{\overleftarrow F}{\longleftarrow} S \stackrel{\overrightarrow F}{\longrightarrow} \mathbb{D} and G : \mathbb{D} \stackrel{\overleftarrow G}{\longleftarrow} T \stackrel{\overrightarrow G}{\longrightarrow} \mathbb{E}, consider the action of their composite on objects: each object of \mathbb{C} may map to multiple objects of \mathbb{E}, via objects of \mathbb{D}. Each such mapping corresponds to a zig-zag path C \longleftarrow s \longrightarrow D \longleftarrow t \longrightarrow E. In order to specify such a path it suffices to give the pair (s,t), which determines C, D, and E. Note, however, that not every pair in S \times T corresponds to a valid path, but only those which agree on the middle object D \in \mathbb{D}. Thus, we may take \{ (s,t) \mid s \in S, t \in T, \overrightarrow{F}(s) = \overleftarrow{G}(t) \} as the set of specifications for the composite F ; G, with \overleftarrow{F ; G}(s,t) = \overleftarrow{F}(s) and \overrightarrow{F ; G}(s,t) = \overrightarrow{G}(t). On morphisms, (F ; G)_{(s,t),(u,v)}(f) = G_{t,v}(F_{s,u}(f)). It is not hard to check that this satisfies the anafunctor laws.

If you know what a pullback is, note that the same thing can also be defined at a higher level in terms of spans. \mathbf{Cat}, the category of all (small) categories, is cocomplete, and in particular has pullbacks, so we may construct a new anafunctor from \mathbb{C} to \mathbb{E} by taking a pullback of \overrightarrow F and \overleftarrow G and then composing appropriately.

One can go on to define ananatural transformations between anafunctors, and show that together these constitute a 2-category \mathbf{AnaCat} which is analogous to the usual 2-category of (small) categories, functors, and natural transformations; in particular, there is a fully faithful embedding of \mathbf{Cat} into \mathbf{AnaCat}, which moreover is an equivalence if AC holds.

To work in category theory based on set theory and classical logic, while avoiding AC, one is therefore justified in “mixing and matching” functors and anafunctors as convenient, but discussing them all as if they were regular functors (except when defining a particular anafunctor). Such usage can be formalized by turning everything into an anafunctor, and translating functor operations and properties into corresponding operations and properties of anafunctors.

However, as I will argue in some future posts, there is a better solution, which is to throw out set theory as a foundation of category theory and start over with homotopy type theory. In that case, thanks to a generalized notion of equality, regular functors act like anafunctors, and in particular AP holds.

References

Makkai, Michael. 1996. “Avoiding the Axiom of Choice in General Category Theory.” Journal of Pure and Applied Algebra 108 (2). Elsevier: 109–73.

Posted in category theory, math, species | Tagged , , , , , , , , , , | Leave a comment

AC and equivalence of categories

This is part three in a series of posts on avoiding the axiom of choice (part one, part two).

In my previous post, I explained one place where the axiom of choice often shows up in category theory, namely, when defining certain functors whose action on objects is specified only up to unique isomorphism. In this post, I’ll explain another place AC shows up, when talking about equivalence of categories. (Actually, as we’ll see, it’s really the same underlying issue, of defining a functor defined only up to unique isomorphism; this is just a particularly important instantiation of that issue.)

When are two categories “the same”? In traditional category theory, founded on set theory, there are quite a few different definitions of “sameness” for categories. Ultimately, this comes down to the fact that set theory does not make a very good foundation for category theory! There are lots of different ideas of equivalence, and they often do not correspond to the underlying equality on sets, so one must carefully pick and choose which notions of equality to use in which situations (and some choices might be better than others!). Every concept, it seems, comes with “strict” and “weak” variants, and often many others besides. Maintaining the principle of equivalence requires hard work and vigilence.

As an example, consider the following definition, our first candidate for the definition of “sameness” of categories:

Two categories \mathbb{C} and \mathbb{D} are isomorphic if there are functors F : \mathbb{C} \to \mathbb{D} and G : \mathbb{D} \to \mathbb{C} such that GF = 1_\mathbb{C} and FG = 1_\mathbb{D}.

Seems pretty straightforward, right? Well, this is the right idea in general, but it is subtly flawed. In fact, it is somewhat “evil”, in that it talks about equality of functors (GF and FG must be equal to the identity). However, two functors H and J can be isomorphic without being equal, if there is a natural isomorphism between them—that is, a pair of natural transformations \phi : H \to J and \psi : J \to H such that \phi \circ \psi and \psi \circ \phi are both equal to the identity natural transformation.1 For example, consider the Haskell functors given by

data Rose a = Node a [Rose a]
data Fork a = Leaf a | Fork (Fork a) (Fork a)

These are obviously not equal, but they are isomorphic, in the sense that there are natural transformations (i.e. polymorphic functions) rose2fork :: forall a. Rose a -> Fork a and fork2rose :: forall a. Fork a -> Rose a such that rose2fork . fork2rose === id and fork2rose . rose2fork === id (showing this is left as an exercise for the interested reader).

Here, then, is a better definition:

Categories \mathbb{C} and \mathbb{D} are equivalent if there are functors F : \mathbb{C} \to \mathbb{D} and G : \mathbb{D} \to \mathbb{C} which are inverse up to natural isomorphism, that is, there are natural isomorphisms GF \cong 1_\mathbb{C} and FG \cong 1_\mathbb{D}.

So the compositions of the functors F and G do not literally have to be the identity functor, but only (naturally) isomorphic to it. This does turn out to be a well-behaved notion of sameness for categories (although you’ll have to take my word for it).

The story doesn’t end here, however. In set theory, a function is a bijection—that is, an isomorphism of sets—if and only if it is both injective and surjective. By analogy, one might wonder what properties a functor F : \mathbb{C} \to \mathbb{D} must have in order to be one half of an equivalence. This leads to the following definition:

\mathbb{C} is proto-equivalent2 to \mathbb{D} if there is a functor F : \mathbb{C} \to \mathbb{D} which is full and faithful (i.e., a bijection on each hom-set) as well as essentially surjective, that is, for every object D \in \mathbb{D} there exists some object C \in \mathbb{C} such that F\ C \cong D.

Intuitively, this says that F “embeds” an entire copy of \mathbb{C} into \mathbb{D} (that’s the “full and faithful” part), and that every object of D which is not directly in the image of F is isomorphic to one that is. So every object of \mathbb{D} is “included” in the image of \mathbb{C}, at least up to isomorphism (which, remember, is supposed to be all that matters).

So, are equivalence and protoequivalence the same thing? In one direction, it is not too hard to show that every equivalence is a protoequivalence: if F and G are inverse-up-to-natural-isomorphism, then they must be fully faithful and essentially surjective. It would be nice if the converse were also true: in that case, in order to prove two categories equivalent, it would suffice to construct a single functor F from one to the other, and show that F has the requisite properties. This often ends up being more convenient than explicitly constructing two functors and showing they are inverse. However, it turns out that the converse is provable only if one accepts the axiom of choice!

To get an intuitive sense for why this is, suppose F : \mathbb{C} \to \mathbb{D} is fully faithful and essentially surjective. To construct an equivalence between \mathbb{C} and \mathbb{D}, we must define a functor G : \mathbb{D} \to \mathbb{C} and show it is inverse to F (up to natural isomorphism). However, to define G we must give its action on each object D \in \mathbb{D}, that is, we must exhibit a function \mathrm{Ob}\ \mathbb{D} \to \mathrm{Ob}\ \mathbb{C}. We know that for each D \in \mathbb{D} there exists some object C \in \mathbb{C} such that F\ C \cong D. That is,

\{ \{ C \in \mathbb{C} \mid F\ C \cong D \} \mid D \in \mathbb{D} \}

is a collection of non-empty sets. However, in a non-constructive logic, knowing these sets are nonempty does not actually give us any objects! Instead, we have to use the axiom of choice, which gives us a choice function \mathrm{Ob}\ \mathbb{D} \to \mathrm{Ob}\ \mathbb{C}, and we can use this function as the object mapping of the functor G.

So AC is required to prove that every protoequivalence is an equivalence. In fact, the association goes deeper yet: it turns out that the statement “every protoequivalence is an equivalence” (let’s call this the Axiom of Protoequivalence, or AP for short) not only requires AC, but is equivalent to it—that is, you can also derive AC given AP as an axiom!

On purely intuitive grounds, however, I would wager that to (almost?) anyone with sufficient category theory experience, it “feels” like AP “ought to be” true. If there is a full, faithful, and essentially surjective functor F : \mathbb{C} \to \mathbb{D}, then \mathbb{C} and \mathbb{D} “ought to be” equivalent. The particular choice of functor G : \mathbb{D} \to \mathbb{C} “doesn’t matter”, since it makes no difference up to isomorphism. On the other hand, we certainly don’t want to accept the axiom of choice. This puts us in the very awkward and inconsistent position of having two logically equivalent statements which we want to respectively affirm and reject. A fine pickle indeed! What to do?

There are four options (that I know of, at least):

  1. If one is feeling particularly rational, one can simply say, “Well, since AC and AP are equivalent, and I reject AC, I must therefore reject AP as well; my feelings about it are irrelevant.”

This is a perfectly sensible and workable approach. It’s important to highlight, therefore, that the “problem” is in some sense more a philosophical problem than a technical one. One can perfectly well adopt the above solution and continue to do category theory; it just may not be the “nicest” (a philosophical rather than technical notion!) way to do it.

We can therefore also consider some more creative solutions!

  1. In a classical setting, one can avoid AC and affirm (an analogue of) AP by generalizing the notion of functor to that of anafunctor (Makkai 1996). Essentially, an anafunctor is a functor “defined only up to unique isomorphism”. It turns out that the appropriate analogue of AP, where “functor” has been replaced by “anafunctor”, is indeed true—and neither requires nor implies AC. Anafunctors “act like” functors in a sufficiently strong sense that one can simply do category theory using anafunctors in place of functors. However, one also has to replace natural transformations with “ananatural transformations”, etc., and it quickly gets rather fiddly.

  2. In a constructive setting, a witness of essential surjectivity is necessarily a function which gives an actual witness C \in    \mathbb{C}, along with a proof that F\ C \cong D, for each D    \in \mathbb{D}. In other words, a constructive witness of essential surjectivity is already a “choice function”, and an inverse functor G can be defined directly, with no need to invoke AC and no need for anafunctors. So in constructive logic, AP is simply true. However, this version of “essential surjectivity” is rather strong, in that it forces you to make choices you might prefer not to make: for each D \in \mathbb{D} there might be many isomorphic C \in \mathbb{C} to choose from, with no “canonical” choice, and it is annoying (again, a philosophical rather than technical consideration!) to be forced to choose one.

  3. Instead of generalizing functors, a more direct solution is to generalize the notion of equality. After all, what really seems to be at the heart of all these problems is differing notions of equality (i.e. equality of sets vs isomorphism vs equivalence…). This is precisely what is done in homotopy type theory (Univalent Foundations Program 2013).3 It turns out that if one builds up suitable notions of category theory on top of HoTT instead of set theory, then (a) AP is true, (b) without the need for AC, (c) even with a weaker version of essential surjectivity that corresponds more closely to essential surjectivity in classical logic.4 This is explained in Chapter 9 of the HoTT book.

I plan to continue writing about these things in upcoming posts, particularly items (2) and (4) above. (If you haven’t caught on by now, I’m essentially blogging parts of my dissertation; we’ll see how far I get before graduating!) In the meantime, feedback and discussion are very welcome!

References

Makkai, Michael. 1996. “Avoiding the Axiom of Choice in General Category Theory.” Journal of Pure and Applied Algebra 108 (2). Elsevier: 109–73.

Univalent Foundations Program, The. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study: http://homotopytypetheory.org/book.


  1. The astute reader may well ask: but how do we know this is a non-evil definition of isomorphism between functors? Is it turtles all the way down (up)? This is a subtle point, but it turns out that it is not evil to talk about equality of natural transformations, since for the usual notion of category there is no higher structure after natural transformations, i.e. no nontrivial morphisms (and hence no nontrivial isomorphisms) between natural transformations. (However, you can have turtles all the way up if you really want.)

  2. I made this term up, since there is no term in standard use: of course, if you accept AC, there is no need for a separate term at all!

  3. As a historical note, it seems that the original work on anafunctors is part of the same intellectual thread that led to the development of HoTT.

  4. That is, using propositional truncation to encode the classical notion of “there exists”.

Posted in category theory, math, species | Tagged , , , , , , , , , | 5 Comments

Unique isomorphism and generalized “the”

This is part two in a series of posts on avoiding the axiom of choice; you can read part one here.

In category theory, one is typically interested in specifying objects only up to unique isomorphism. In fact, definitions which make use of actual equality on objects are sometimes referred to (half-jokingly) as evil. More positively, the principle of equivalence states that properties of mathematical structures should be invariant under equivalence. This principle leads naturally to speaking of “the” object having some property, when in fact there may be many objects with the given property, but all such objects are uniquely isomorphic; this cannot cause confusion if the principle of equivalence is in effect.

This phenomenon should be familiar to anyone who has seen simple universal constructions such as terminal objects or categorical products. For example, an object 1 \in \mathbb{C} is called if there is a unique morphism A \to 1 from each object A \in \mathbb{C}. In general, there may be many objects satisfying this criterion. For example, in \mathbf{Set}, the category of sets and functions, every singleton set is terminal: there is always a unique function from any set A to a singleton set \{\star\}, namely, the function that sends each element of A to \star. However, it is not hard to show that any two terminal objects must be uniquely isomorphic1. Thus it “does not matter” which terminal object we use—they all have the same properties, as long as we don’t do anything “evil”—and one therefore speaks of “the” terminal object of \mathbb{C}. As another example, a product of two objects A,B \in \mathbb{C} is a diagram A \stackrel{\pi_1}{\longleftarrow} C \stackrel{\pi_2}{\longrightarrow} B with the universal property that any other C' with morphisms to A and B uniquely factors through C. Again, there may be multiple such products, but they are all uniquely isomorphic, and one speaks of “the” product A \times B.

Note that in some cases, there may be a canonical choice among isomorphic objects. For example, this is the case with products in \mathbf{Set}, where we may always pick the Cartesian product \{(a,b) \mid a \in A, b \in B\} as a canonical product of A and B (even though there are also other products, such as \{(b,a) \mid a \in A, b \in B\}). In such cases use of “the”, as in “the product of A and B”, is even more strongly justified, since we may take it to mean “the canonical product of A and B”. However, in many cases (for example, with terminal objects in \mathbf{Set}), there is no canonical choice, and “the terminal object” simply means something like “some terminal object, it doesn’t matter which”.

Beneath this seemingly innocuous use of “the” (often referred to as generalized “the”), however, lurks the axiom of choice! For example, if a category \mathbb{C} has all products, we can define a functor P : \mathbb{C} \times \mathbb{C} \to \mathbb{C}2 which picks out “the” product of any two objects A and B—indeed, P may be taken as the definition of the product of A and B. But how is P to be defined? Consider \{ \mathrm{Prod}(A,B) \mid A,B \in \mathbb{C} \}, where \mathrm{Prod}(A,B) denotes the set of all possible products of A and B, i.e. all suitable diagrams A \stackrel{\pi_1}{\longleftarrow} C \stackrel{\pi_2}{\longrightarrow} B in \mathbb{C}. Since \mathbb{C} has all products, this is a collection of nonempty sets; therefore we may invoke AC to obtain a choice function, which is precisely P_0, the action of P on objects. The action of P on morphisms may then be defined straightforwardly.

The axiom of choice really is necessary to construct P: as has already been noted, there is, in general, no way to make some canonical choice of object from each equivalence class. On the other hand, this seems like a fairly “benign” use of AC. If we have a collection of equivalence classes, where the elements in each class are all uniquely isomorphic, then using AC to pick one representative from each really “does not matter”, in the sense that we cannot tell the difference between different choices (as long as we refrain from evil). Unfortunately, even such “benign” use of AC still poses a problem for computation.


  1. If you have never seen this proof before, I highly recommend working it out for yourself. Given two terminal objects X and Y, what morphisms must exist between them? What can you say about their composition? You will need to use both the existence and uniqueness of morphisms to terminal objects.

  2. Note that we have made use here of “the” product category \mathbb{C} \times \mathbb{C}—fortunately \mathbf{Cat}, like \mathbf{Set}, has a suitably canonical notion of products.

Posted in category theory, math, species | Tagged , , , , , , , , | 8 Comments

Avoiding the axiom of choice, part I

I’m hard at work on my dissertation, and plan to get back to doing a bit of blogging based on stuff I’m writing and thinking about, as a way of forcing myself to explain things clearly and to potentially get some useful feedback. Yes, this means you can expect more on species! But first, I’ll write a few posts about the axiom of choice and anafunctors, which have turned out to be fundamental to some of the work I’ve been doing. If you look at the nLab page for anafunctors, linked above, you could be forgiven for thinking this is a pretty esoteric corner of category theory, but in fact it’s not too bad once you grasp the essentials, and is quite relevant for anyone interested in category theory and constructive/computational foundations (such as homotopy type theory (HoTT)).

The Axiom of Choice

The (in)famous Axiom of Choice (hereafter, AC) can be formulated in a number of equivalent ways. Perhaps the most well-known is:

The Cartesian product of any collection of non-empty sets is non-empty.

Given a family of sets \{X_i \mid i \in I\}, an element of their Cartesian product is some I-indexed tuple \{x_i \mid i \in I\} where x_i \in X_i for each i. Such a tuple can be thought of as a function (called a choice function) which picks out some particular x_i from each X_i.

The Axiom of Choice in type theory, take 1

We can express this in type theory as follows. First, we assume we have some type I which indexes the collection of sets; that is, there will be one set for each value of type I. Given some type A, we can define a subset of the values of type A using a predicate, that is, a function P : A \to \star (where \star denotes the universe of types). For some particular a : A, applying P to a yields a type, which can be thought of as the type of evidence that a is in the subset P; a is in the subset if and only if P\ a is inhabited. An I-indexed collection of subsets of A can then be expressed as a function C : I \to A \to \star. In particular, C(i,a) is the type of evidence that a is in the subset indexed by i. (Note that we could also make A into a family of types indexed by I, that is, A : I \to \star, but it wouldn’t add anything to this discussion.)

A set is nonempty if it has at least one element, so the fact that all the sets in C are nonempty can be modeled by a dependent function which yields an element of A for each index, along with a proof that it is contained in the corresponding subset.

(i : I) \to (a : A) \times C(i,a)

(Note I’m using the notation (x:X) \to T(x) for dependent function types instead of \prod_{x:X} T(x), and (x:X) \times T(x) for dependent pairs instead of \sum_{x:X} T(x).) An element of the Cartesian product of C can be expressed as a function I \to A that picks out an element for each I (the choice function), together with a proof that the chosen elements are in the appropriate sets:

(g : I \to A) \times ((i : I) \to C(i, g(i)))

Putting these together, apparently the axiom of choice can be modelled by the type

((i : I) \to (a : A) \times C(i,a)) \to (g : I \to A) \times ((i : I) \to C(i, g(i)))

Converting back to \Pi and \Sigma notation and squinting actually gives some good insight into what is going on here:

\left( \prod_{i : I} \sum_{a : A} C(i,a) \right) \to \left( \sum_{g : I \to A} \prod_{i : I} C(i, g(i)) \right)

Essentially, this says that we can “turn a (dependent) product of sums into a (dependent) sum of products”. This sounds a lot like distributivity, and indeed, the strange thing is that this is simply true: implementing a function of this type is a simple exercise! If you aren’t familiar with dependent type theory, you can get the intuitive idea by implementing a non-dependent Haskell analogue, namely something of type

(i -> (a,c)) -> (i -> a, i -> c).

Not too hard, is it? (The implementation of the dependent version is essentially the same; it’s only the types that get more complicated, not the implementation.) So what’s going on here? Why is AC so controversial if it is simply true in type theory?

The Axiom of Choice in type theory, take 2

This is not the axiom of choice you’re looking for. — Obi-Wan Funobi

The problem, it turns out, is that we’ve modelled the axiom of choice improperly, and it all boils down to how non-empty is defined. When a mathematician says “S is non-empty”, they typically don’t actually mean “…and here is an element of S to prove it”; instead, they literally mean “it is not the case that S is empty”, that is, assuming S is empty leads to a contradiction. (Actually, it is a bit more subtle yet, but this is a good first approximation.) In classical logic, these viewpoints are equivalent; in constructive logic, however, they are very different! In constructive logic, knowing that it is a contradiction for S to be empty does not actually help you find an element of S. We modelled the statement “this collection of non-empty sets” essentially by saying “here is an element in each set”, but in constructive logic that is a much stronger statement than simply saying that each set is not empty.

(I should mention at this point that when working in HoTT, the best way to model what classical mathematicians mean when they say “S is non-empty” is probably not with a negation, but instead with the propositional truncation of the statement that S contains an element. Explaining this would take us too far afield; if you’re interested, you can find details in Chapter 3 of the HoTT book, where all of this and much more is explained in great detail.)

From this point of view, we can see why the “AC” in the previous section was easy to implement: it had to produce a function choosing a bunch of elements, but it was given a bunch of elements to start! All it had to do was shuffle them around a bit. The “real” AC, on the other hand, has a much harder job: it is told some sets are non-empty, but without any actual elements being mentioned, and it then has to manufacture a bunch of elements out of thin air. This is why it has to be taken as an axiom; we can also see that it doesn’t fit very well in a constructive/computational context. Although it is logically consistent to assume it as an axiom, it has no computational interpretation, so anything we define using it will just get stuck operationally.

So, we’ll just avoid using AC. No problem, right?

Don’t look now, but AC is behind you

The problem is that AC is really sneaky. It tends to show up all over the place, but disguised so that you don’t even realize it’s there. You really have to train yourself to think in a fundamentally constructive way before you start to notice the places where it is used. Next time I’ll explain one place it shows up a lot, namely, when defining functors in category theory (though thankfully, not when defining Functor instances in Haskell).

Posted in category theory, math, species | Tagged , , , , , | 17 Comments

Diagrams 1.0

The diagrams team is very pleased to announce the 1.0 release of diagrams, a framework and embedded domain-specific language for declarative drawing in Haskell. Check out the gallery for some examples of what it can do. Diagrams can be used for a wide range of purposes, from data visualization to illustration to art, and diagrams code can be seamlessly embedded in blog posts, LaTeX documents, and Haddock documentation, making it easy to incorporate diagrams into your documents with minimal extra work.

       

What’s new

Brent recently gave a talk at the New York Haskell Users’ Group presenting the new release. You can find videos of the talk on vimeo: part 1 presents a basic introduction to the library, and part 2 talks about mathematical abstraction and DSL design. The slides are also available.

This release includes a number of significant new features and improvements. Highlights include:

  • Support for drawing arrows between given points or between diagrams, with many options for customization (tutorial, documentation, API).

  • A new framework for creating custom command-line-driven executables for diagram generation (tutorial, API).

  • Offsets of trails and paths, i.e. compute the trail or path lying a constant distance from the given one (documentation, API).

  • A new API, based on Metafont, for constructing cubic splines with control over things like tangents and “tension” (tutorial, API).

  • Tangent and normal vectors of segments and trails (API).

  • Alignment can now be done by trace in addition to envelope (API).

  • The lens package is now used consistently for record fields throughout the library (documentation).

  • Across-the-board improvements in performance and size of generated files.

See the release notes for full details, and the migration guide for help porting your diagrams 0.7 code to work with diagrams 1.0.

Try it out

For the truly impatient:

cabal install diagrams

Diagrams is supported under GHC 7.4 and 7.6.

To get started, read the quick start tutorial, which will introduce you to the fundamentals of the framework and provide links for further reading.

For those who are less impatient and want to really dig in and use the power features, read the extensive user manual. There is also a growing collection of tutorials on specific topics.

Get involved

Diagrams has a friendly and growing community of users and developers. To connect with the community, subscribe to the project mailing list, and/or come hang out in the #diagrams IRC channel on freenode.org for help and discussion. Development continues stronger than ever, and there are a wide range of projects available for new contributors of all levels of Haskell skill. Make some diagrams. Fix some bugs. Submit your cool examples for inclusion in the gallery or your cool code for inclusion in the diagrams-contrib package.

Happy diagramming!

Brought to you by the diagrams team:

  • Daniel Bergey
  • Jeff Rosenbluth
  • Ryan Yates
  • Brent Yorgey

with contributions from:

  • Jan Bracker
  • Conal Elliott
  • Daniil Frumin
  • Sam Griffin
  • Niklas Haas
  • Peter Hall
  • Claude Heiland-Allen
  • Deepak Jois
  • John Lato
  • Felipe Lessa
  • Chris Mears
  • Ian Ross
  • Carlos Scheidegger
  • Vilhelm Sjöberg
  • Michael Sloan
  • Jim Snavely
  • Luite Stegeman
  • Kanchalai Suveepattananont
  • Michael Thompson
  • Scott Walck
Posted in diagrams, haskell, projects | Tagged , , | 2 Comments

Catsters guide

tl;dr: http://byorgey.wordpress.com/catsters-guide-2/

In an attempt to solidify and extend my knowledge of category theory, I have been working my way through the excellent series of category theory lectures posted on Youtube by Eugenia Cheng and Simon Willerton, aka the Catsters.

Edsko de Vries used to have a listing of the videos, but it is no longer available. After wresting a copy from a Google cache, I began working my way through the videos, but soon discovered that Edsko’s list was organized by subject, not topologically sorted. So I started making my own list, and have put it up here in the hopes that it may be useful to others. Suggestions, corrections, improvements, etc. are of course welcome!

As far as possible, I have tried to arrange the order so that each video only depends on concepts from earlier ones. Along with each video you can also find my cryptic notes; I make no guarantee that they will be useful to anyone (even me!), but hopefully they will at least give you an idea of what is in each video.

I have a goal to watch two videos per week (at which rate it will take me about nine months to watch all of them); I will keep the list updated with new video links and notes as I go.

Posted in haskell, math, teaching | Tagged | 1 Comment

In defense of drawing by coding

Just some half-baked thoughts in repsonse to Bret Victor’s talk, Drawing Dynamic Visualizations (along with his addendum here). As usual, it is a fun and inspiring talk, so if you haven’t seen it I highly recommend it; but I will summarize it here.

He starts by surveying the state-of-the-art in options for the creative scientist who wants to visualize some data. The options he outlines are:

  1. Use some program like Excel which has a standard repertoire of graphs it can generate. The problem with this approach is that it completely stifles any creativity and freedom in visualizing data.

  2. Use a drawing program like Illustrator or Inkscape. This gives more freedom, of course, but the process is tedious and the results cannot easily be modified.

  3. The final option is to write some code in a framework like Processing or d3.js. The problem here, Victor says, is that you are just staring at a mass of symbols with no immediate, dynamic feedback.

He then goes on to demo a really cool prototype tool that allows drawing using a graphical interface, a bit like Illustrator or Inkscape. But the similarity is only surface deep: where those programs are restrictive and inflexible, Victor’s is richly interactive and editable. Instead of drawing concretely located lines, circles, and so on, it infers the relationships between things you are drawing, so updating the characteristics or positioning of one element automatically updates all the others which depend on it as well. In other words, one can construct a generic, editable visualization just by drawing one particular example of it.

Victor is quite negative about option (3) above—drawing by coding—referring to programming as “blindly manipulating symbols”: “blind” because you can’t actually see the picture you are creating while writing the program.

What I would like to point out is that in fact, despite his negativity about drawing by programming, when using his graphical tool Victor is still programming! It’s just that he has a graphical interface which allows him to construct certain sorts of programs, instead of writing the programs directly. In fact, you can see the programs he constructs on the left side of the screen in his tool. They appear to be structured imperative programs, consisting of sequences of drawing instructions together with things like loops and conditionals.

The problem is that this kind of higher-level interface cannot provide for all possible circumstances (unless you somehow make it Turing complete, but in that case it probably ceases to be at all intuitive). For example, Victor impressively drags and drops some spreadsheet data into his application. But what if I want to use data which is structured in some other format? What if I need to preprocess the data in some computationally nontrivial way? Or on the drawing end, what if I want to draw some shapes or compute some positions in a way that the interface does not provide for? We can’t completely get away from the need to write code in the service of visualization.

What we really need is a more inclusive idea of “programming”, and a continuum between direct manipulation of images and manipulation of symbols to produce images. Symbolic methods, of course, can be incredibly powerful—there is nothing inherently wrong with manipulating symbols.

More specifically, I am proposing something like the following:

  1. First, I am all for making elegant and powerful high-level graphical interfaces for constructing interactive, editable drawings—and not just drawings but code that generates drawings. This can probably be pushed quite far, and there is lots of HCI research to be done here. There are also some very interesting questions relating to bidirectional computation here: making an edit via the graphical interface corresponds to some sort of edit to the code; how can this be done in a sensible and consistent way?

  2. Recognizing, however, that sometimes you do need to actually write some code, how can we make the underlying language as beautiful as possible, and how can we make the interaction between the two systems (code and higher-level graphical interface) as elegant and seamless as possible? The ideal is for a user to be able to flow easily back and forth between the two modes, ideally spending much of their time in a high-level graphical mode.

Of course, if you hadn’t guessed by now, in the long term this is the sort of direction I would love to go with diagrams… though I need to finish my dissertation first (more on that subject soon).

Posted in diagrams | Tagged , , , , , , , | 3 Comments