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 complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration 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 nforum 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).

nLab > Latest Changes: Awodey's proposal

Bottom of Page

1 to 15 of 15

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeMar 13th 2019

    now that Mike announced a proof, and hearing Steve’s comment, I felt it would be nice to have a name for conjecture (partially) proven thereby, for ease of communiucating it to the rest of the world. Just a start, please edit the entry as need be.

    v1, current

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 13th 2019

    What of the elementary/Grothendieck distinction? Who first articulated claims about what this distinction means for the internal logic?

    And when do we get to see slides, or better a recording, Mike?

    • CommentRowNumber3.
    • CommentAuthorAli Caglayan
    • CommentTimeMar 13th 2019

    Here are the slides of Mike’s second talk. I don’t think there exists a better recording apart from the one Felix took.

    • CommentRowNumber4.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 13th 2019

    So the strict univalent universes correspond to which type universes out of: Russell, Tarski, weak Tarski ? I guess not the last… Or is this an orthogonal notion? This should be made explicit in the page where Mike’s results are discussed.

    • CommentRowNumber5.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 13th 2019

    And what was Steve’s comment?

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeMar 13th 2019

    Steve just highlighted that it’s a breakthrough (on the off-chance that anyone didn’t get it) and amplified that it finally goes to confirm his 10 year old conjecture.

  7. this was not a precise conjecture, but more of a research proposal.

    steveawodey

    diff, v3, current

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeMar 14th 2019

    upon request, I added pointer to p. 9 of

    diff, v5, current

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeMar 14th 2019

    Re #4, I would say these universes correspond most directly to strictly Tarski ones, although the distinction between Russell and strict-Tarski universes is mostly lost when passing from syntax to categorical models (even strict ones such as CwFs). I think the usual way to interpret Russell universes is to first “desugar” them to Tarski universes and then interpret those.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeMar 14th 2019

    I don’t have time to add it right now, but we should also be clear about the difference between the conjectures “type theory can be interpreted in all Grothendieck (∞,1)(\infty,1)-toposes” and “the homotopy theory of type theories is equivalent to the homotopy theory of elementary (∞,1)(\infty,1)-toposes”. The former is what I announced, but the latter is still quite open, although Kapulkin-Sumilo have proven the analogue for (∞,1)(\infty,1)-categories with finite limits, corresponding to type theories with Σ\Sigma and identity types only, no Π\Pis or universes, and it seems likely that the tools I used in the Grothendieck case may be useful in proving versions of the stronger conjecture.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeMar 14th 2019

    Also here are my slides from the Midwest HoTT last weekend, which have some more detail. I’m hoping to put up the preprint within a week or two.

    • CommentRowNumber12.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 14th 2019

    @Mike thanks!

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeOct 31st 2020
    • (edited Oct 31st 2020)

    completed publication data for:

    diff, v10, current

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeJun 17th 2022

    added pointer to:

    diff, v11, current

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeJun 17th 2022

    I have expanded the paragraph starting with “A concise statement is…” (here).

    diff, v11, current

1 to 15 of 15

  1.