On Thu, Jan 19, 2012 at 2:05 PM, Bertfried Fauser wrote: > Dear Bill, > >> The only thing missing here is the concept of sub-object (sub-domain) >> and how it should interact with logic, otherwise the underlying structure >> of the language would essentially be a topos (algebraic set theory). >> And a lot (maybe almost all of mathematics or at least the constructive >> part of mathematics?) can be done as internal structures of such a >> mathematical category. > > Hm, can you make that statement more precise? [I am much interested > still in this issue] >
I was afraid that you were still reading and that you might ask ... :) > I would like to warn you that `topos valid' mathematics is probably > not what people in computer algebra (or Bishop) would call > 'constructive'. While the logic is weaker, it still has some sort of > existential quantifier, which allows you to state existence > without being able to 'generate' such an object. Such a situation, > many people would call non-constructive. Granted. "constructive part" was meant to soften my claim. > There are quite a few mathematicians which do not see a topos as a > sort of set theory, but look at them much more as a theory of spaces. > Also I guess your topos is an elementary topos not a Grothendieck > topos?. > Yes, elementary topos. I am interested only in the axioms which are intended to capture set theory "algebraically". I am interested in topos as a foundation in the sense of set theory. Rather than answer your specific request to be more precise now, let me mention a related paper that I am reading at the moment: http://arxiv.org/abs/1112.1284 Relative Frobenius algebras are groupoids Chris Heunen, Ivan Contreras, Alberto S. Cattaneo (Submitted on 6 Dec 2011) We functorially characterize groupoids as special dagger Frobenius algebras in the category of sets and relations. This is then generalized to a non-unital setting, by establishing an adjunction between H*-algebras in the category of sets and relations, and locally cancellative regular semigroupoids. Finally, we study a universal passage from the former setting to the latter. -- This paper is about Frobenius algebras in the category of sets and relations. It is the first time I have seen both groupoids and Frobenius algebra in the same title! Have you read this? 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.
