Johnstone and Wraith "Algebraic Theories in Toposes" (in LNM 661, 1978) looked at algebraic theories (limited to single sorted in their discussion) in elementary toposes with NNO. This is also in the Elephant vol II, in D5.3. See in particular Theorem D5.3.5, which expresses the existence of algebras freely generated by sets of generators. It's kind of obvious that many (not all) of their methods work equally well for many sorted cartesian (essentially algebraic) theories though to my embarrassment I can't find a clear reference this instant. You can also find notes in Section 4.1 of my draft chapter "Locales and Toposes as Spaces" for the Handbook of Spatial Logic, available at http://www.cs.bham.ac.uk/~sjv/LocTopSpaces.pdf A general result covers situations where there are two such theories T1 and T2 with a theory morphism between them (mapping sorts to sorts, symbols to symbols, axioms to axioms). If E is an elementary topos with NNO then the forgetful functor Mod_E(T2) -> Mod_E(T1) between categories of models in E has a left adjoint. (Surely this is already published? But in any case Palmgren and I know how to prove it.) Clearly the general result includes as a special case the existence of an NNO. This covers your question about path categories, i.e. free categories over graphs. The theories T1 and T2 of graphs and of categories are both cartesian, with two sorts for objects and arrows. In fact T1 is many-sorted algebraic, though T2 is not algebraic because composition of arrows is only a partial operation. There's an obvious theory morphism T1 -> T2. Exercise: Show how to construct path categories in an elementary topos with NNO! You might need to construct list objects first, using the fact that a finite list over X is a function from {1,...,n} to X for some natural number n. Steve Vickers. Galchin Vasili wrote:
--- Steve Vickers <s.j.vickers@cs.bham.ac.uk> wrote:
In topos-valid constructivism the way it works is this. In an arbitrary elementary topos you can't always construct the free categories over graphs. But as soon as you admit a natural numbers object other free algebra constructions, such as the free category, come along with it.
Steve, can you expand here and point at a source for reading. I.e. as soon as you admit an NNO, then other comes along with it. Can you expand on this?
Regards, Bill
14-Jun-2005 13:30:22 -0300,1147;000000000000-00000010