nLab sharp modality

Definition

On a local topos/local (∞,1)-topos $\mathbf{H}$, hence equipped with a fully faithful extra right adjoint $coDisc$ to the global section geometric morphism $(Disc \dashv \Gamma)$, is induced an idempotent monad $\sharp \coloneqq coDisc \circ \Gamma$, a modality which we call the sharp modality. This is itself the right adjoint in an adjoint modality with the flat modality $\flat \coloneqq Disc \circ \Gamma$.

In type theory

We assume a dependent type theory with crisp term judgments $a::A$ in addition to the usual (cohesive) type and term judgments $A \; \mathrm{type}$ and $a:A$, as well as context judgments $\Xi \vert \Gamma \; \mathrm{ctx}$ where $\Xi$ is a list of crisp term judgments, and $\Gamma$ is a list of cohesive term judgments. A crisp type is a type in the context $\Xi \vert ()$, where $()$ is the empty list of cohesive term judgments. In addition, we also assume the dependent type theory has typal equality and judgmental equality.

From here, there are two different notions of the sharp modality which could be defined in the type theory, the strict sharp modality, which uses judgmental equality in the computation rule and uniqueness rule, and the weak sharp modality, which uses typal equality in the computation rule and uniqueness rule. When applied to a type they result in strict sharp types and weak sharp types respectively. The natural deduction rules for strict and weak sharp types are provided as follows:

• Formation rule for weak and strict sharp types:

$$\frac{\Xi, \Gamma \vert () \vdash A \; \mathrm{type}}{\Xi \vert \Gamma \vdash \sharp A \; \mathrm{type}}\sharp-\mathrm{form}$$

• Introduction rule for weak and strict sharp types:

$$\frac{\Xi, \Gamma \vert () \vdash a:A}{\Xi \vert \Gamma \vdash a^\sharp:\sharp A}\sharp-\mathrm{intro}$$

• Elimination rule for weak and strict sharp types:

$$\frac{\Xi \vert () \vdash a:\sharp A}{\Xi \vert \Gamma \vdash a_\sharp:A}\sharp-\mathrm{elim}$$

• Computation rule for weak and strict sharp types respectively:

$$\frac{\Xi \vert () \vdash a:A}{\Xi \vert \Gamma \vdash \beta_{\sharp A}(a):(a^\sharp)_\sharp =_A a}\sharp-\mathrm{comp}\mathrm{weak} \qquad \frac{\Xi \vert () \vdash a:A}{\Xi \vert \Gamma \vdash (a^\sharp)_\sharp \equiv a:A}\sharp-\mathrm{comp}\mathrm{strict}$$

• Uniqueness rule for weak and strict sharp types respectively:

$$\frac{\Xi \vert () \vdash a:\sharp A}{\Xi \vert \Gamma \vdash \eta_{\sharp A}(a):(a_\sharp)^\sharp =_{\sharp A} a}\sharp-\mathrm{uniq}{weak} \qquad \frac{\Xi \vert () \vdash a:\sharp A}{\Xi \vert \Gamma \vdash (a_\sharp)^\sharp \equiv a:\sharp A}\sharp-\mathrm{uniq}\mathrm{strict}$$

Weak sharp modalities are primarily used in cohesive weak type theories, while strict sharp modalities are typically used in cohesive type theories which are not weak, such as cohesive Martin-Löf type theory (cohesive homotopy type theory or cohesive higher observational type theory.

Properties

Relation to discrete and codiscrete objects

• The codiscrete objects in a local topos are the modal types for the sharp modality.

• The discrete objects in a local topos are the modal types for the flat modality.

Related concepts

• sharp excluded middle

cohesion

• (shape modality $\dashv$ flat modality $\dashv$ sharp modality)

  $(\esh \dashv \flat \dashv \sharp )$

  • discrete object, codiscrete object, concrete object

  • points-to-pieces transform

  • structures in cohesion

• dR-shape modality$\dashv$ dR-flat modality

  $\esh_{dR} \dashv \flat_{dR}$

infinitesimal cohesion

• classical modality

tangent cohesion

• differential cohomology diagram

differential cohesion

• (reduction modality $\dashv$ infinitesimal shape modality $\dashv$ infinitesimal flat modality)

  $(\Re \dashv \Im \dashv \&)$

  • reduced object, coreduced object, formally smooth object

  • formally étale map

  • structures in differential cohesion

graded differential cohesion

• fermionic modality$\dashv$ bosonic modality $\dashv$ rheonomy modality

  $(\rightrightarrows \dashv \rightsquigarrow \dashv Rh)$

singular cohesion

$$\array{ && id &\dashv& id \\ && \vee && \vee \\ &\stackrel{fermionic}{}& \rightrightarrows &\dashv& \rightsquigarrow & \stackrel{bosonic}{} \\ && \bot && \bot \\ &\stackrel{bosonic}{} & \rightsquigarrow &\dashv& \mathrm{R}\!\!\mathrm{h} & \stackrel{rheonomic}{} \\ && \vee && \vee \\ &\stackrel{reduced}{} & \Re &\dashv& \Im & \stackrel{infinitesimal}{} \\ && \bot && \bot \\ &\stackrel{infinitesimal}{}& \Im &\dashv& \& & \stackrel{\text{étale}}{} \\ && \vee && \vee \\ &\stackrel{cohesive}{}& \esh &\dashv& \flat & \stackrel{discrete}{} \\ && \bot && \bot \\ &\stackrel{discrete}{}& \flat &\dashv& \sharp & \stackrel{continuous}{} \\ && \vee && \vee \\ && \emptyset &\dashv& \ast }$$

References

The terminology of the sharp-modality in the above sense was introduced – in the language of $(\infty,1)$-toposes and as part of the axioms on “cohesive $(\infty,1)$-toposes” – in:

• Urs Schreiber, Differential cohomology in a cohesive $\infty$-topos (2013)

See also the references at local topos.

Early discussion in view of homotopy type theory and as part of a set of axioms for cohesive homotopy type theory is in

• Mike Shulman, Urs Schreiber, Quantum gauge field theory in Cohesive homotopy type theory (2014)

The dedicated type theory formulation with “crisp” types, as part of the formulation of real cohesive homotopy type theory, is due to:

• 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)