Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 20th 2011

    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.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeJan 20th 2011

    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.

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 20th 2011

    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 Grpd\infty-Grpd. 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.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeJan 20th 2011

    Well, I would say the point is that a (normal) monic in a homotopy category need not be a monic in the (,1)(\infty,1)-category it came from. Monomorphisms in Gpd\infty Gpd are, up to equivalence, just the inclusions of subsets of connencted components.

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 21st 2011

    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.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeJan 21st 2011

    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.

    • CommentRowNumber7.
    • CommentAuthorDavidRoberts
    • CommentTimeJan 22nd 2011

    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.