Warning- this post is just my recent thoughts about math. I don't know how to make them rigorous, and they may be completely wrong.

I've been thinking about how the subfields of math each center around the theory of some object. The object is normally given as a set theoretic construction satisfying some axioms, and the field of study is concerned with the properties of these objects, what objects in other fields satisfy the axioms (and are therefore part of the field), and with transformations between the chosen objects. Category theory in some sense captures this idea by making the objects of study this situation- a category can be thought of as containing the objects of some field of study, the morphisms are the transformation between the objects. Categories can just be thought of as another object, defined like any other field's chosen object, but they can be considered the embodiment of a field of mathematics. This makes it a little less surprising (though not much, this is pretty surprising!) that categories are so intimately related to theories (the object "a theory" consisting of types, function symbols, axioms, and relation symbols). In fact, the "internal language" of a category is a theory, and the model of a theory is a category. This is an amazing thing that I'm just beginning to grasp, really.

In most theories of some object, there are important properties that we want to show that a particular object has. In group theory, for example, we want a set to have, among other things, an identity element for it to be a group. The group homomorphism from the one element group to a given group points out that identity element, and therefore the one element group embodies the property of identity. The proof that a group has an identity is then embodied in the existence of a homomorphism between the group that embodies the identity and the chosen group.

What I'm wondering is- how general is this idea? Are all properties of objects embodied in some object, and all proofs embodied in the existence of morphisms from that object? In closed categories, where the morphism are objects of the category, this means that the theory of the objects of the category contain their own proofs. This seems like Topos theory, which requires a couple more properties then just being closes, which studies categories that have enough structure to contain systems of mathematics (as I understand it). Not all categories contain their morphisms in this way, and so not all theories contain their proofs, but it looks like Topos and their associated theories do this.

Interestingly being closed appears to be fundamental to categorical notions of computation. The categories whose theories are type systems over the lambda calculus are Cartisian closed categories, although I think that can be weakened in some ways. This is a basic fact of computation it seems- Turing machines have their universal Turing machines which run encoding of other machines, lambda terms are defined over other lambda terms, and actual machines can't distinguish (in general) between data and code. The whole Howard-Curry isomorphism and proofs as propositions interpretation gives us the fact that programs encode proofs of a proposition in some system of logic (in the case of the lambda calculus, lambda terms can be read as programs to be reduced, or as proofs. It just depends on how you read them). It seems to me that in a constructive mathematics all proofs would indeed be some form of transformation which can be encoded in an object (functors, homomorphism groups, etc) meaning that objects and their proofs are the same thing. This puts a perspective on things like naive set theory- if you can describe objects that don't make sense (contradictory sets) then you have to expect contradictory proofs. It may be that the safest thing to found a system of mathematics on is something where we can construct all objects, where the transformations between objects are contained in the theory, and therefore we can construct the object embodying all proofs (if we couldn't construct it, it wouldn't be true).

I normally ignore the philosophy of constructive mathematics as my interest in it is really just as a computer scientist. I think of math as being a human activity, so classical logic isn't really "wrong" and people are welcome to do it if they want (it is certainly powerful, even if its a bit odd at times). On the other hand, it does seem that constructive math, as I understand it, is on a good foundation where it safely contains its own proofs and its lack of freedom in defining objects (as opposed to classical math where we can define some very strange things) prevents the weirdness of classical math. Type theory started as a way to prevent set theoretic paradoxes, and intuitionistic type theory may be the way to go for a system of math that constrains its objects and proofs enough to keep math down to earth.

Okay, enough ranting. Sorry for the half formed thoughts, but I wanted to record them somewhere.