In partial answer to Oege de Moor's query concerning the uniqueness of strength in non-well-pointed finite product categories ... there is an, admittedly, special case when the strength is unique: namely when the type F is a strong initial (or final) datatype. The strength can be described as a fold (or unfold) and the uniqueness of this guarantees the uniqueness of the strength (actually this is dependent on the uniqueness of the strengths of the functors over which the datatype is defined ... which inductively one assumes are datatypes). Strong datatypes were described in "Strong Catgeorical Datatypes I" by myself and Dwight Spencer (p 141-169, Category Theory 1991) - also see Dwights thesis. More recently Bart Jacobs has given an alternative treatment which elides much of the fibrational and 2-categorical aspects present in our treatment. There are besides various other circumstances which force strengths to be unique. E.g. if F is cartesian over a functor G with a unique strength (that is there is a strong natural transformation F --> G with all naturality squares pullbacks) then its strength is uniquely determined. These observations were made in "Data III" (with Dwight: an unpublished follow on to the yet unpublished "Data II"!!) and were recently sharpened when Barry Jay visited here (Calgary). BUT does anyone have an example of a functor with a non-unique strength? -robin (Robin Cockett) +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
participants (1)
-
robin@cpsc.ucalgary.ca