Yes, Michael has said in several papers that his foundation would be given in FOLDS. And perhaps some specific version of the axioms has been given in some paper that I have missed. But I do not know of it; and when Martin-Löf suggested last year that I might want to pursue a type-theoretic foundation for category theory he did not mention knowing of one existing yet. So far as I know it remains a project. best, Colin 2010/5/26 John Baez <baez@math.ucr.edu>:
Colin wrote:
As to articulating a way to avoid ever using identity of objects and
identity of categories, John Baez writes
I think Michael Makkai has done it. He has formulated a foundational approach to mathematics based on infinity-categories, in which equality plays no fundamental role:
http://www.math.mcgill.ca/makkai/mltomcat04/mltomcat04.pdf
I think some approach along these general lines might ultimately become quite popular.
But so far as know, this remains an approach, and not any specific set of axioms offered as foundation.
I should let Michael speak for himself, but I have the impression that he intends to found all his work on FOLDS - "first-order logic with dependent sorts". In this paper:
http://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf
he writes:
"The restriction on the use of equality in FOLDS is a fundamental feature. FOLDS is to be used in formulating categorical situations in which, for example, equality of objects of a category is not an admissible primitive. The absence of term-forming operators, to be interpreted as functions, is a consequence of the absence of equality; it seems to me that the notion of "function" is incoherent without equality.
It is convenient to regard FOLDS a logic without equality entirely, and deal with equality, as much as is needed of it, as extralogical primitives."
Best, jb
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]