[FOM] Formalization Thesis

[Andre.Rodin@ens.fr]

Selon Messing <messing at math.umn.edu>:

> First a minor point, a final object in a category C is not a colimit,
> but rather a limit over the empty category.

sure, I didn't mean a final object is a colimit but just put my question for
both limits and colimits.

> Concerning "up
> to canonical isomorphism",  it is not clear to me that the term
> "canonical" has a sufficiently precise meaning, except that given to it,
> by Bourbaki, in the (now suppressed) appendix to chapitre IV of Theorie
> des Ensembles, 1958 edition.

By "canonical" I mean here "unique" (as usual).



>In dealing with fibered or cofibered
> categories, one has to specify for each pair of composable morphisms in
> the base category, the natural equivalence between (gf)* and f*g*, this
> being subject to the axioms Grothendieck introduced in Seminaire
> Bourbaki, expose 190 and SGA 1, expose VI.  In the context of monoidal
> categories one has to impose the pentagon axiom, and in  symetric
> monoidal categories, the hexagon  axiom as well.

I discuss this in my paper on identity mentioned in the previous posting. But I
cannot see how these features relate to Formalisation Thesis.

best,
andrei