[FOM] Formalization Thesis
Andre.Rodin at ens.fr
Mon Jan 7 17:49:34 EST 2008
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.
More information about the FOM