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.
I have finally split off dependent sum from dependent product. And added a few more paragraphs.
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.
Is that a little confusing at dependent sum to have it be left adjoint to base change for any $f:A \to I$, then later consider only terminal maps?
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 \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?
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.
pointer
On first inspection, this Bonart article is not directly about what’s covered on this page.
1 to 9 of 9