Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
If we follow Mike’s suggestion at internal logic of an (infinity, 1)-topos that we distinguish type theory from logic, and treat the latter as “about constructing subobjects”, then is there a reason to look at one rather than another of monomorphisms, regular monomorphisms, effective monomorphisms, normal monomorphisms and corresponding subobjects, or even Freyd’s generalized normal subobjects or generalized regular subobjects, as in Homotopy is not concrete.
I would say that any kind of monomorphism you pick can have its own logic. For instance, quasitoposes have two kinds of internal logic: one for monics, and one for regular=strong monics. More generally, all you need for “a logic” is a fibration in preorders.
That said, for toposes and related categories, it generally seems to be the plain monomorphisms whose logic carries the most information. For 1-toposes, every monic is regular and effective, but that probably fails in higher topoi.
Thanks. I was trying to come up with a concrete example to illustrate the internal logic of an (infinity, 1)-topos and thinking about subobjects of (the fundamental infinity group of) the 2-sphere in . I was surprised to read Freyd’s argument that the 2-sphere in the homotopy category of pointed spaces has more than a set’s worth of generalized normal subobjects. Perhaps that’s a step too far for a logic.
Well, I would say the point is that a (normal) monic in a homotopy category need not be a monic in the -category it came from. Monomorphisms in are, up to equivalence, just the inclusions of subsets of connencted components.
I seem to be being rather dim about all this. How about we take a network of streets in a city. Then there are very many homotopy classes of paths from A to B. In the same class are to be found efficient paths and variants which allow for long detours and retracings. Predicates must respect classes. So I can’t have as a predicate ’passes through C’, but I can have ’passes through C, and all homotopic paths pass through C’, perhaps to be termed ’necessarily passes through C’. But this isn’t the logic of city life, as I might very well want to get from A to B via C, and C be up a cul-de-sac so that for any solution there’s a homotopic path which avoids C. The predicate ’possibly passes through C’ could apply to a class which contains a path passing through C, but in a connected grid that applies to every path class.
I guess the lesson is that this homotopy logic isn’t what’s wanted in the city. Maybe it’s not surprising, though, that modalities are near at hand, given possible world semantics and their accessibility relations.
I guess the lesson is that this homotopy logic isn’t what’s wanted in the city.
Yes, I agree. Homotopy logic only makes sense when you honestly can’t tell the difference between homotopic paths.
Well, to specifically refer to a C in your travels in the city is non-kosher, because any point accessible from C is isomorphic to C in the fundamental groupoid, and you shouldn’t specify a specific element of an isomorphism class.
1 to 7 of 7