added ISBN to

- Robert Geroch,
*Mathematical Physics*, Chicago 1985 (ISBN:9780226223063)

and DOI to

- Marco Grandis,
*Category Theory and Applications: A Textbook for Beginners*, World Scientific 2021 (doi:10.1142/12253)

Added a reference to Joyal’s CatLab.

]]>added publication data for

- Birgit Richter,
*From categories to homotopy theory*, Cambridge Studies in Advanced Mathematics 188, Cambridge University Press 2020 (doi:10.1017/9781108855891, book webpage, pdf)

As suggested on another thread, I have added in a reference to the list of networks of category theorists. It could be useful.

]]>Added a reference to lectures on category theory by Peter Johnstone.

]]>Raymond, if you have javascript disabled and are not using a browser such as Firefox which can render MathML, you may encounter this. To render mathematics one needs one of the two.

]]>I have removed the “other texts”-label.

]]>replaced the dead link to Barr-Wells TTT with a link to the TAC reprint. Also I wonder why it is listed under “other texts”.

]]>Do you mean a specific entry, or is it the $n$Lab in general that does not display properly on your system?

I just checked the entry *category theory*, and – except for some bad whitespaces, which I have fixed now – it renders properly on my system.

Can this be corrected?

Regards,

Raymond Boute ]]>

Mention additional non-mathematical applications of CT; reference ’applied category theory’ page.

]]>Add link to Grandis’s textbook

]]>I still want to know in the progression of the modalities why jets rather than germs?. Should minimality tell us which?

]]>Well, density is something that can be expressed internally.

]]>Ignoring the Hegelese, is this not a mathematical use of minimality at Aufhebung?

]]>…the Aufhebung of $\emptyset\dashv \ast$ is necessarily given by a

densesubtopos $\mathcal{E}_j$. Since the double negation topology $\neg\neg$ is the unique largest dense topology it follows in general that $\mathcal{E}_{\neg\neg}\subseteq\mathcal{E}_j$ , in particular in the case that $\mathcal{E}_{\neg\neg}$ happens to be essential and hence happens to be a level, the minimality condition on the Aufhebung of the initial opposition means that $\mathcal{E}_j = \mathcal{E}_{\neg\neg}$ is, in particular, a Boolean topos.

I’m glad Dan’s talk was helpful, Urs!

]]>the minimality aspect of the progression couldn’t be represented in 2-DTT.

Is there any *mathematical* use for that minimality?

Type theory seems to have that effect.

By the way, where you hope in #29

Maybe there could be a type theory which is adjoint-to-the-roots that would be able to more seamlessly admit implementation of progressions of adjoint modalities as needed for super-differential cohesion.

I asked something to that effect on the blog, and Mike pointed out that the minimality aspect of the progression couldn’t be represented in 2-DTT.

]]>Okay, this morning I heard Dan Licata’s very nice talk (here) on LSR and followup developments. Towards the end it had something about the “Modal theory of Dependent type theory”, which seems to be exactly the kind of thing I was expressing hope, above, should exist, and should help with defining adjoint modalities in DTT.

I don’t quite understand now the way the discussion worked out here (apparently various misunderstandings) but I am very happy to see this take shape!

]]>Oh, I see now: The text at the beginning of 2.2 is referring to the *boxed* items in Fig. 2.2.

Spotted another typo: In the first displayed equation in the proof of theorem 6.7 on p. 31, “$\beta_m$” should be “$\beta_m/x_m$”.

And if I were an editor I’d remark:

In the statement of theorem 6.7, expand “the syntax” to say which syntax exactly.

add a table of contents

I generally find type theory hard to read, but isn’t it just that the first line of Fig. 2 records the first kind of judgement concerns assignments of modes to types, followed by generating rules for mode assignment, starting with propositions $P$. Then the second line records the second kind of judgement concerns assignments of mode contexts to contexts, followed by generating rules, starting with the empty context being assigned the empty mode context.

]]>Hi Mike, I am reading LSR. I have trouble matching the text of the first two paragraphs of section 2.2 to Figure 2, which supposedly they should be referring to.

Could you check? In the text, does “the first judgement” and “the second judgement” refer to the top left two items in figure 2? Could you explain how? Even the symbol names don’t seem to match.

]]>Re #48

some kind of “syntax for dependently typed multivariable adjunctions”,

do you have some examples of such adjunctions appearing “in nature”?

Maybe indexed adjunctions?

]]>Re #38: I’m not sure what you mean. You can have a hyperdoctrine with the usual quantification adjoints to substitution maps (as mentioned in #27), but without additive disjunction (= coproducts) in the “fibers”. So within a specific hyperdoctrine, I wouldn’t say that additive disjunction is necessarily a special case of existential quantification.

If all you mean is that additive disjunction is an example of a Kan extension, and that Kan extensions are adjoints to certain types of substitution maps, then of course I agree with that.

]]>