nLab bireflective subcategory




By a bireflective subcategory one might mean:

  1. A subcategory ι:𝒞\iota \,\colon\, \mathcal{C} \hookrightarrow \mathcal{B} which is both reflective and coreflective — i.e. a fully faithful functor possessing both left and right adjoints: LιRL \dashv \iota \dashv R (reflective localization and coreflective localization).

    Such subcategories are called essential localizations by Kelly & Lawvere (1989), following the terminology of essential geometric morphisms from topos theory, see also at level of a topos.

    The adjoint pair ιLιR\iota \circ L \dashv \iota \circ R is then an adjoint modality; see there for more.

  2. More specifically, one may in addition ask that LRL \simeq R, hence that the subcategory inclusion ι\iota has an ambidextrous adjoint βιβ\beta \dashv \iota \dashv \beta.

    Such subcategories are called quintessential localizations by Johnstone (1996).

    The corresponding (co-)monad ιβ\natural \coloneqq \iota \circ \beta is then a Frobenius monad (see at classical modality).

  3. Finally, one may moreover ask that the points-to-pieces transform ϵidη\natural \overset{\epsilon}{\longrightarrow} id \overset{\eta}{\longrightarrow} \natural of a quintessential localization be the identity morphisms.

    This strong form of the notion is the case actually called bireflective subcategories by Freyd et al. (1999).



A full subcategory-inclusion

ι:𝒞 \iota \;\colon\; \mathcal{C} \hookrightarrow \mathcal{B}

is bireflective in the sense of FOPTST99, Def. 8 iff

(1.) the inclusion has an ambidextrous adjoint

(2.) such that for all EE \in \mathcal{B} the counit of the right adjunction followed by the unit of the left adjunction (the points-to-pieces transform) equals the identity:


The first clause in Def. does not in general by itself enforce the second clause. A counter-example is given in FOPTST99, Rem. 12.

However, the second clause does follow automatically when \mathcal{B} is a Cauchy-complete category (Johnstone (1996)).


In the other direction, the second clause in Def. implies that

is an idempotent natural endomorphism, exhibited as a split idempotent.


Given a category \mathcal{B}, its bireflective subcategories (Def. ) are in correspondence with the split idempotent natural endomorphisms on id id_\mathcal{B} with specified splitting, i.e.


(1)η ϵ =id. \eta^\natural \,\circ\, \epsilon^\natural \;=\; \mathrm{id} \,.

(FOPTST99, Thm. 13)

Concretely, from a split idempotent on id id_{\mathcal{B}} we recover the Frobenius monad \natural as follows:


Given a split idempotent transformation as in Prop. we have for all EE \,\in\, \mathcal{B}

(η E )=η E and(ϵ E )=ϵ E . \natural (\eta^{\natural}_{E}) \;=\; \eta^{\natural}_{\natural E} \;\;\;\;\;\; \text{and} \;\;\;\;\;\; \natural (\epsilon^{\natural}_{E}) \;=\; \epsilon^{\natural}_{\natural E} \,.

(RFL21, Lem. 7.7)

By naturality of the transformation η\eta

and using (1) we get the first statement:

(η E )=(η E )η E ϵ E id E=η E η E ϵ E =η E \natural (\eta^{\natural}_{E}) \;=\; \natural (\eta^{\natural}_{E}) \circ \overset { \mathrm{id}_E } { \overbrace{ \eta^\natural_E \circ \epsilon^\natural_E } } \;=\; \eta^\natural_{\natural E} \circ \eta^{\natural}_{E} \circ \epsilon^\natural_E \;=\; \eta^{\natural}_{\natural E}

The second follows analogously.


Given a split idempotent transformation as in Prop. , :\natural \colon \mathcal{B} \to \mathcal{B} becomes

  1. an idempotent monad (,η,μ)(\natural, \eta, \mu) by setting

    μ(ϵ () ) \mu \,\coloneqq\, \natural(\epsilon^\natural_{(-)})
  2. an idempotent comonad (,ϵ,δ)(\natural, \epsilon, \delta) by setting

    δ(η () ) \delta \,\coloneqq\, \natural(\eta^\natural_{(-)})

(RFL21, Prop. 7.8)

For the associativity of the monoid product we need to show the commutativity of

By functoriality of \natural this follows from the commutativity of

which holds by naturality of ϵ\epsilon.

The other claims follow similarly.

Modal type theory

A modal type theory for bireflection modalities has been proposed in Riley, Finster & Licata (2021), Riley (2022).

We show the inference rules which these authors propose to add to plain intuitionistic type theory for encoding the presence of a bireflection classical modality \natural on the type system, and we show corresponding categorical semantics via commuting diagrams in an interpreting locally cartesian closed category (a more syntactic semantics is indicated in RFL21, Sec. 7, esp. Fig. 6).


Given a bireflection :\natural \colon \mathcal{B} \to \mathcal{B} as above, then for Γ\Gamma \in \mathcal{B} we obtain a monad on the slice category, to be denoted

(2) Γ: /Γ /Γ \natural_\Gamma \;\colon\; \mathcal{B}_{/\Gamma} \to \mathcal{B}_{/\Gamma}

by setting

Γ[A p A Γ](η Γ ) *[A p A Γ] \natural_\Gamma \left[ \begin{array}{c} A \\ \big\downarrow \mathrlap{\!\! {}^{p_A} } \\ \Gamma \end{array} \;\;\;\; \right] \;\;\coloneqq\;\; \big(\eta^\natural_\Gamma\big)^\ast \,\natural\, \left[ \begin{array}{c} \natural A \\ \big\downarrow \mathrlap{\!\! {}^{\natural p_A} } \\ \natural \Gamma \end{array} \;\;\;\; \right]


Beware of some non-obvious properties of the following type-theoretic syntax:

  1. There is an asymmetry in the meaning of ()̲\underline{(-)}:

    An underline of a context denotes application of \natural, but an underline of a type in context only means its pullback along the counit ϵ \epsilon^{\natural}. The idea is that underlines indicate dependency on \natural-modal variables, to be distinguished of a type itself being \natural-modal or not.

  2. The syntactic symbol “\natural” is not exactly interpreted as the bireflective monad of that name. Rather:

    • An unadorned “\natural” in the syntax interprets, in context Γ\Gamma, as the relative monad

      classical Γ rel: /Γ (η Γ ) * /Γ Γ /Γ \classical^{rel}_\Gamma \;\; \colon \;\; \array{ \mathcal{B}_{/\natural \Gamma} & \xrightarrow{ (\eta^\natural_\Gamma)^\ast } & \mathcal{B}_{/\Gamma} & \xrightarrow{ \natural_\Gamma } & \mathcal{B}_{/\Gamma} }
    • The combination ()̲\natural \underline{(-)} is what actually interprets as Γ\natural_\Gamma (2).

      This transpires syntactically in RFL21, Cor. 2.14; Riley22, Cor. 1.1.16, and semantically in (3) below.

The list of inference rules and their categorical semantics (first the axioms then derived rules):

Using these ingredients, one finds that the function aa̲ a \,\mapsto\, \underline{a}^\natural is interpreted simply as postcomposition with the η \eta^{\natural}-naturality square:

(3) \;

With this, one finds the following rule for \natural respecting dependent pair types:

(4) \;

Using this one finds that every type AA is the dependent sum type of its fiber linear types A x̲A_{\underline{x}} (NB: we show 1-categorical semantics, interpreting identification types as diagonal morphisms):

(5) \;



(spaces among retractive spaces)
Let \mathcal{B} be the category of retractive topological spaces (or just of Sets), i.e. the category of diagrams in Top (Set) of the form BiEpBB \xrightarrow{i} E \xrightarrow{p} B such that pi=id Bp \circ i \,=\, id_B. Then the functor

Top Top B [BidBidB] \begin{array}{ccc} Top &\hookrightarrow& Top_{\mathcal{R}} \\ B &\mapsto& \big[ B \xrightarrow{id} B \xrightarrow{id} B \big] \end{array}

is a bireflective subcategory inlusion (Def. ) with ambidextrous adjoint given by

Top Top [BiEpB] B \begin{array}{ccc} Top_{\mathcal{R}} &\longrightarrow& Top \\ \big[ B \xrightarrow{i} E \xrightarrow{p} B \big] &\mapsto& B \end{array}


(zero-vector bundles among all vector bundles)
For any ground field, let Vect Set SSetVectS\mathcal{B} \coloneqq Vect_{Set} \coloneqq \int_{S \in Set} Vect S be the category VectBund of vector bundles over Sets, hence of indexed vector spaces. Then the functor

Set0Vect Set Set \xhookrightarrow{\;\; 0 \;\;} Vect_{Set}

which sends any set SS to the zero vector bundle S×{0}S \times \{0\} over SS is a bireflective subcategory in the sense of Def. .


(zero-spectrum bundles among all parameterized spectra)
Let TGrpd T Grpd_\infty denote the \infty -category of parameterized spectra over varying \infty -groupoids (the tangent \infty -category of Grpd Grpd_\infty ). Then the inclusion

Grpd TGrpd Grpd_\infty \hookrightarrow T Grpd_\infty

given by sending XGrpd X \in Grpd_\infty to the zero-spectrum bundle over XX ought to count as a “bireflective sub- \infty -category” (cf. here at infinitesimal cohesion).

A model category-presentation of this situation by a (left and right) Quillen functor to a model structure for parameterized spectra underlying which is a bireflective sub-1-category inclusion (Def. ) may be recognized in Hebestreit, Sagave & Schlichtkrull (2020), Lem. 3.19, there incarnated as the canonical inclusion

𝒮 Sp Σ \mathcal{S}^{\mathcal{I}} \hookrightarrow Sp^{\Sigma}_{\mathcal{R}}

of \mathcal{I} -spaces into symmetric spectra internal to retractive spaces (Exp. ).

An analogous statement is in Braunack-Mayer (2019), Cor. 2.45.


On subcategory inclusion which have both a left and a right adjoint (essential localizations):

  • G. M. Kelly, F. W. Lawvere, On the complete lattice of essential localizations, Bull. Soc. Math. Belg. Sér. A 41 (1989) 289–319 [pdf]

On subcategory inclusions with ambidextrous adjoints (quintessential localizations):

On subcategory inclusions with ambidextrous adjoints whose points-to-pieces transform is the identity (actual bireflective subcategories):

Discussion of a modal type theory for bireflective modalities, in a context of linear homotopy type theory:

Last revised on April 17, 2023 at 11:16:58. See the history of this page for a list of all contributions to it.