Re: Re: terminology

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

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.

In this paper Michael defines "multitopic ω-category" more or less
analogously to how Eilenberg and Mac~Lane defined "category," and he
defines "the (large) multitopic set of all
(small) multitopic ω-categories" using that definition.  If I
understand these correctly (and have not, for example, confused
intuitive motivation with strict definition) they take for granted
such as ideas as the category Set of sets, and Set-valued functors.

While Eilenberg and Mac~Lane saw (and referred to) the foundational
significance of their ideas, they did not offer their definition as a
foundation per se.  And they were right.   Lawvere's foundations ETCS
and CCAF are first-order axiomatizations which suffice to prove the
theorems of mathematics (exactly which theorems depending on exactly
which axioms, but he clearly defined variants suited to classical
analysis and various extensions of that).

Has anyone yet offered a  first-order (or ML-typetheoretic)
axiomatization of mathematics along Makkai's lines?

Popular is another question!   And I am not worried about finding a
final form of such axioms.  But I do not yet know of such axioms.

best, Colin

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]