Re: terminology

[Colin McLarty <colin.mclarty@case.edu>]

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/ ]