On Wed, Dec 3, 2008 at 4:51 PM, Ralf Hemmecke wrote: > > ... > But then there is the general problem. In category theory > everything happens 'up to isomorphism', in particular uniqueness. >
That is not entirely true. There are many statements about morphisms that involve strict equality, e.g. any commutative diagram is such a statement. In addition, universal properties like limits specifically require that certain morphisms exist and are *unique*. For example, consider the definition of 'coerce' as "the pullback of an injection along a retraction". The relationship between such a coercion and retraction is exact. Perhaps it is true that the relationship between domains (objects) in a given category is defined only "up to an isomorphism". But there are alternative descriptions/categories where this is not true. See: http://planetmath.org/encyclopedia/CategoryTheory.html "Isomorphism is in fact a central notion in category theory: most categorical constructions cannot distinguish between isomorphic objects. Frequently, this is exactly what is desired, since equality of objects is in general a tricky concept: if we take a group and replace each element with a pair, that element and a "tag", do we have the same group? Strictly speaking, no, but they are certainly isomorphic. Of course, sometimes one wants to distinguish between isomorphic objects: the different Sylow $ p$-subgroups of a finite group, for example. In such a case, the category-theoretic solution is to work in a different category (called an arrow category) where the objects are now morphisms of the original category (in the example of subgroups of a given group, the objects would be injections of a subgroup into a larger group). This allows one to describe exactly the difference between the isomorphic objects: they are embedded in a larger group in different ways." > Do you have a suggestion how you would handle that > > Record(a: A, b: B) > > is 'isomorphic' with > > Record(b: B, a: A)? > > Or, if you like take Cross and don't include the tags a and b. > This is a consequence of the definition of Record as a categorical product. > Similarly you had this isomorphism problem in your last mail... > > NonNegativeInteger = Union(Zero(Integer),PositiveInteger) > > You must give the compiler a chance to generate exactly the same > code for both sides. > Thanks for correcting the example. Yes I agree that here it is a problem. I do not know how to proceed to make this literally true. But a domain construction like that used with SubDomain seems like it should be possible. > Until I read a paper that rigorously proves that the topos view on SPAD > makes for a better language, I don't believe it. > I think it is necessary to explain what you mean by "a better language". It seems obvious to me that a language that has a clear and well-defined semantics is (usually) better than one in which the various linguistic constructions are simply ad hoc. Even better it seems to me is if this semantics has a clear relationship to the immediate intended application of the language, i.e. to the expression of mathematical concepts. Regards, Bill Page. --~--~---------~--~----~------------~-------~--~----~ You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To post to this group, send email to [email protected] To unsubscribe from this group, send email to [EMAIL PROTECTED] For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en -~----------~----~----~----~------~----~------~--~---
