Sorry!

Harrison Grodin

]]>52: I also see filled-in circles on mine

]]>Re #52, no not on mine.

]]>For some reason, the `\bigcirc`

on this page is displayed as a *filled-in* circle in my browser. Does anyone else see that?

Removed idempotence and (co)monadicity from the definition, since there are plenty of non-idempotent and even non-(co)monadic modalities.

]]>Thanks. Notice that this entry “modality” is a bit of a disambiguation entry, the dedicated page for modal homotopy type theory is modal homotopy type theory. I’ll copy over your addition to there.

]]>Added the various definitions of a modality from RSS.

]]>I guess the “open modality” Ex 1.7 of Modalities in HoTT ($\bigcirc_P (X) = P \to X$) is the reader monad for a proposition.

]]>Whoops. Will fix.

]]>Then $Adj(K)$ is composed of 2-functors $Adj \to K$.

For some meaning of “composed of”, but it’s not the functor category $K^Adj$: its objects are the objects of $K$, and its *morphisms* are the functors $Adj \to K$.

So $Adj(Adj(K))$, adjoint triples in $K$, is also $K^{Adj \times Adj}$. I guess that makes $Adj(Adj(Cat))$ a dependent type 2-theory, since these concern maps $\mathcal{M}^{op} \times Adj \to Cat$.

]]>Emily Riehl has $\mathbf{Adj}$ as the walking adjunction here, saying this comes from Schanuel-Street.

Makes sense. Then $Adj(K)$ is composed of 2-functors $Adj \to K$.

]]>Yes, the choice of right vs left adjoints is a convention. In fact LS and LSR use different conventions.

Maybe $K\mapsto Adj(K)$ would be 2-category of adjunctions? Or just Adj.

]]>Oh, I see, sorry. And only now do I see the reply in #37.

]]>I think Mike was wondering what I meant by #34.

]]>what exactly is the question you’re asking?

The question was in #32:

]]>Which entry would sensibly host the following definition? I am inclined to have this under “modality” in a section “In category theory” with the understanding that more refined definition exists and will follow. But let me know if anyone has strong opinions about this.

Yes #34 was rather a muddle, but if there is a question there it’s perhaps about the orientations of the 2-categories, e.g., is the choice of right adjoints in $radj$ just a convention?

Are there standard names associated with $K \mapsto Adj(K)$?

]]>Re #34, what exactly is the question you’re asking?

Re #35, yes, there’s an operation $K \mapsto Adj(K)$ on 2-categories. I agree, we should have a page about this.

]]>Since this is a purely category-theoretic definition, I would put it at reflective subcategory or idempotent monad. A category-theoretic terminology for the functor itself would be “reflector”. In certain contexts this could be called simply a “modality” (e.g. the HoTT Book), but the notion of modality is more general than this, so I would not want to put this forward as if it were *the* definition on page modality.

To be specific, the kind of material that, I think, would usefully be spelled out in – or at least linked to from – relevant entries (many of which are lacking any indication of details) is the (basic) stuff written out here.

Terminology may be changed, of course, but let’s not get this debate too much in the way of the content.

]]>So that’s a general process, right, where a 2-category is sent to the 2-category of adjunctions within it. Reapplying this map, a morphism in the resulting 2-category is an adjoint triple in the original 2-category.

]]>Could better naming be suggested by the Shulman-Licata-Riley approach? Modal logic is the logic associated to *modes*, which feature in a 2-category. But has this settled yet?

In Adjoint Logic with a 2-Category of Modes: A pseudofunctor from a 2-category of modes, $\mathcal{M}$ to $\mathbf{Adj}$, the 2-category of categories, adjunctions, and conjugate natural transformations.

We don’t seem to have an nLab page on such a 2-category.

Then in Mike’s HoTTEST talk, it’s $\mathcal{M}^{op} \to \mathcal{C}a t_{radj}$. Why these choices?

]]>We had a learned discussion about ’comodality’ back here, and I thought the consensus was opposed to it and in favour of ’comonadic modality’.

]]>I am going to spell out some elementary basics regarding (co)reflective subcategories and (co)modal/(co)localization endofunctors, on the $n$Lab, lecture note style. Which entry would sensibly host the following definition? I am inclined to have this under “modality” in a section “In category theory” with the understanding that more refined definition exists and will follow. But let me know if anyone has strong opinions about this.

Consider

an endofunctor

$\bigcirc \;\colon\; \mathcal{D} \to \mathcal{D}$whose full essential image we denote by

$Im(\bigcirc) \overset{\phantom{AA} \iota \phantom{AA}}{\hookrightarrow} \mathcal{D}$-
$X \overset{\eta_X}{\longrightarrow} \bigcirc X$
for all objects $X \in \mathcal{D}$, to be called the

*unit morphism*;such that:

for every object $Y \in Im(\bigcirc) \hookrightarrow \mathcal{D}$ in the essential image of $\bigcirc$, every morphism $f$ into $Y$ factors

$\array{ && X \\ & {}^{\mathllap{ \eta_X }}\swarrow && \searrow^{\mathrlap{f}} \\ \mathrlap{\bigcirc X\;\;\;\;} && \underset{\exists !}{\longrightarrow} && Y & \in Im(\bigcirc) }$*uniquely*through the unit

Dually:

a

*comodal operator on $\mathcal{D}$*isan endofunctor

$\Box \;\colon\; \mathcal{D} \to \mathcal{D}$whose full essential image we denote by

$Im( \Box ) \overset{\phantom{AA} \iota \phantom{AA}}{\hookrightarrow} \mathcal{D}$-
$\Box X \overset{ \epsilon_X }{\longrightarrow} X$
for all objects $X \in \mathcal{D}$, to be called the

*counit morphism*;

such that:

for every object $Y \in Im( \Box ) \hookrightarrow \mathcal{D}$ in the essential image of $\Box$, every morphism $f$ out of $Y$ factors

$\array{ && X \\ & {}^{\mathllap{\epsilon_X}}\nearrow && \nwarrow^{\mathrlap{f}} \\ \mathrlap{\Box X\;\;\;} && \underset{\exists !}{\longleftarrow} && Y \in Im( \Box ) }$*uniquely*through the counit