added pointer also to this exposition:

- David Jaz Myers,
*Simplicial, Differential, and Equivariant Homotopy Type Theory*, talk at CQTS (Jan 2023) [video: rec]

Dunno. The analogous pair for simplicial+smooth cohesion does commute (thm. 6.1.3 on p. 30 of Myers & Riley)

]]>Does any interesting non-commutativity appear elsewhere?

]]>Maybe to amplify that they “they commute” but “don’t communicate” may sound stronger than it is: In “commuting” orbisingular + real cohesion, the shape modality does *not* commute with the orbi-singular modality, and in this non-commutativity lies the distinction between geometric and homotopy fixed points and thus the whole content of equivariant homotopy theory.

Morning thought.

Re #30, I was reminded of our discussion of cohesive and equivariant modalities back here:

they commute with each other. But currently they don’t communicate with each other.

In the intro to the new paper they contrast commuting with nesting. Is there a communicating which isn’t just a nesting?

]]>while I was at it, I have tried to bring the Idea-section and the References-section into better shape.

The material in between these two seems somewhat random and may need attention. Good that the entry still carries the warning label “under construction”.

]]>added pointer to today’s

- David Jaz Myers, Mitchell Riley,
*Commuting Cohesions*[arXiv:2301.13780]

added pointer to

- Mike Shulman,
*Comonadic modalities and cohesion*, talk at*Geometry in Modal Homotopy Type Theory*, 2019 (pdf slides, talk recording)

added full publication data for

- Mike Shulman,
*Brouwer’s fixed-point theorem in real-cohesive homotopy type theory*, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)

here and elsewhere

]]>I thought so when I wrote #25, but now I think maybe there is no problem. Of course a *small* set of morphisms can’t be stable under pullback or products, so my question wasn’t quite correctly phrased. The subtlety, IIRC, is that the “internal localization” at an arbitrary class $S$ is the “external localization” at the stabilization of $S$ under pullbacks or products, rather than $S$ itself. But if the external localization at a set $S$ is *known* to be an exponential ideal, then the class of morphisms that it inverts is necessarily stable under products; thus the internal localization agrees with the external one. Similarly, if the external localization is left exact, then the class of morphisms it inverts is pullback-stable. And I think we can play a similar game for subcategories with stable units, although in that case the class of *all* inverted morphisms may not be pullback-stable.

Thanks, I see.

So I suppose you are well aware of this proposition which states that an accessible reflective sub-$\infty$-category of an accessible $\infty$-category is given by localization at a small set of morphisms.

But I guess it may be nontrivial to combine this with pullback stability.

]]>So back here I argued that every exponential ideal is a localization at some class $S$ closed under finite products, and every reflective subcategory with stable units is a localization at some pullback-stable class $S$, but I ignored size issues. Is it true, if all the $\infty$-categories and functors involved are accessible, that these classes $S$ can be chosen to be small?

(By an “internal family of maps” I mean rather than a set or class $S$ of maps in the external sense, we have an object $S$ of the topos and a map $X\to Y$ in $\mathbf{H}/S$. This is what the HIT construction of localization actually uses. But I’m pretty sure that this is strictly more general than a small external family, since we can always take $S$ to be a coproduct of copies of 1.)

]]>All the modalities arising in topos models of cohesion are accessible, correct?

You may have to help me, do you mean that the underlying $\infty$-functors are accessible? In that case the answer is yes.

But you mention localization at an internal family of maps. This I don’t know about. Could you give me some pointer to more details?

]]>No, no weakly Tarski universes. I’m still hoping that we’ll find a way to model honest universes in all toposes. Plus I have faith that most anything we do with honest universes could be done more tediously with weakly Tarski ones, and the library is intended to be usable.

Right now I am wondering whether anything important would be lost by restricting attention to accessible modalities (those obtained by localization at some internal family of maps). All the modalities arising in topos models of cohesion are accessible, correct? The only inaccessible modality that I can think of is “double-negation in the absence of propositional resizing”, and accessible ones have a number of advantages both actual and technical. (In particular, right now I think the theorem that the type of modal types for a lex modality is itself modal only works in the accessible case; I was too sloppy with universes when I proved it before using type-in-type).

And no, I never heard any more from Gallozzi since June.

]]>@Urs is this thesis generally available? Googling Gallozzi’s name didn’t produce much of use.

]]>Interesting.

Do you also include aspects of weak Tarskian universes in the redesign?

I suppose you did see the final version of Cesare Gallozzi’s thesis recently? (I am asking because I only know that you were involved to some extent, but not how much exactly.)

]]>Nice!

I’m currently working on a bunch of redesigns of the HoTT/Coq library, part of my goal being to make it easier to redo the theory of modalities and cohesion therein. We already have some of it, but some is left to do, e.g. the theory of lex modalities. It’ll have to be mostly rewritten from scratch, but it’ll be better for that, and more usable in the future given all that we’ve learned in the current incarnation of the library.

]]>Alexander Berenbeim just started a blog on cohesive homotopy type theory

]]>I have updated the links to Mike’s code at *cohesive homotopy type theory*, alerted by this discussion

Ah, I see. Thanks.

]]>Done.

]]>Yes, the existence of Type, or more particularly its consequence that we can talk about “functions from types to types”, is what I referred to above as “parametric polymorphism”.

Ah, thanks, I never knew what that term meant. So “parametric” for “may vary/depend over the base/context” and “polymorphism” since there is more than one type? Is that just what it means?

Maybe we can put a note into *parametric polymorphism*.

Yes, the existence of $Type$, or more particularly its consequence that we can talk about “functions from types to types”, is what I referred to above as “parametric polymorphism”. Haskell doesn’t have a “type classifier” like Coq does, but we can still define a “function from types to types” by defining a “type that depends on a type variable” — this is how you do a monad. What I meant by “any strongly typed language has monads” was that even without such polymorphism, there still “exist” monads on the category of types, such as those one constructs in Haskell — it’s just that you won’t be able to define the monad as a single entity within the language syntax.

]]>Thanks! Great.

One last question for tonight (local time):

Any strongly typed language “has monads”

Hm, so in Coq, the way you coded it at least, the crucial bit is the Type classifier, the internal incarnation of the type universe, which allows to explicitly give the endomorphism of the monad

$\sharp : Type \to Type \,.$Not all these languages will have such a type of types, right?

]]>