Tag Archives: isomorphism

Anafunctors

Posted on June 16, 2014 by Brent

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 … Continue reading →

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

AC and equivalence of categories

Posted on June 5, 2014 by Brent

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 … Continue reading →

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

Unique isomorphism and generalized “the”

Posted on May 13, 2014 by Brent

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 … Continue reading →

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

Counting linear lambda terms: choice and correspondence

Posted on February 8, 2011 by Brent

In my last post, I showed how to write down polymorphic types with numbers of linear inhabitants given by products of factorials and Mersenne numbers, but left open the question of types with five linear inhabitants in particular, and whether … Continue reading →

Posted in combinatorics | Tagged , , , , | 1 Comment