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

Discussion Tag Cloud

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: dependent sum

Bottom of Page

1 to 9 of 9

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeOct 2nd 2012

    I have finally split off dependent sum from dependent product. And added a few more paragraphs.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2014

    Added a section Relation to some limits with the remarks that dependent sum to the points preserves fiber products and that the naturality squares of the unit are pullbacks.

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 5th 2017

    Is that a little confusing at dependent sum to have it be left adjoint to base change for any f:A→If:A \to I, then later consider only terminal maps?

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 7th 2018

    Returning to my comment in #3, do type theorists use the terms dependent sum (or pair) and dependent product for adjoints to base change for general f:A→Bf: A \to B, or only for terminal maps?

    Does anyone know the history of this? When did Martin-Löf first talk about dependent sum/product? Would he use the terms in the more general sense?

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeJun 7th 2018

    I don’t know the history. In general, dependent sum/product are used in type theory for syntax that corresponds to adjoints to base change along a display map (i.e. to a map with terminal codomain, but in an arbitrary context). But since every map is isomorphic (in extensional type theory) or equivalent (in homotopy type theory) to a display map, in category theory we tend to use the words for adjoints to base change along an arbitrary map.

    • CommentRowNumber6.
    • CommentAuthorHurkyl
    • CommentTimeMar 3rd 2021

    Added the relevant construction for infinity categories.

    diff, v16, current

    • CommentRowNumber7.
    • CommentAuthorperezl.alonso
    • CommentTimeApr 15th 2024

    pointer

    • Peter Bonart. Towards a General Theory of Dependent Sums (2024). (arXiv:2404.08139).

    diff, v18, current

    • CommentRowNumber8.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 15th 2024

    On first inspection, this Bonart article is not directly about what’s covered on this page.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeApr 15th 2024
    • (edited Apr 15th 2024)

    added warning to the Idea-section that “sum” in “dependent sum” is really referring to coproducts

    and added a warning before the reference to Bonart

    diff, v19, current

1 to 9 of 9

  1.