nLab flat modality

Contents

Contents

Definition

On a local topos/local (∞,1)-topos H\mathbf{H}, hence with extra fully faithful right adjoint coDisccoDisc to the global section geometric morphism (DiscΓ)(Disc \dashv \Gamma), is canonically induced the idempotent comonad DiscΓ\flat \coloneqq Disc\circ \Gamma. This modality sends for instance pointed connected objects BG\mathbf{B}G to coefficients BG\flat \mathbf{B}G for flat principal ∞-connections, and may therefore be referred to as the flat modality. It is itself the left adjoint in an adjoint modality with the sharp modality coDiscΓ\sharp \coloneqq coDisc \circ \Gamma. If H\mathbf{H} is in addition a cohesive (∞,1)-topos then it is also the right adjoint in an adjoint modality with the shape modality \int.

In type theory

We assume a dependent type theory with crisp term judgments a::Aa::A in addition to the usual (cohesive) type and term judgments AtypeA \; \mathrm{type} and a:Aa:A, as well as context judgments Ξ|Γctx\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 flat modality which could be defined in the type theory, the strict flat modality, which uses judgmental equality in the computation rule and uniqueness rule, and the weak flat modality, which uses typal equality in the computation rule and uniqueness rule. When applied to a type they result in strict flat types and weak flat types respectively. The natural deduction rules for strict and weak flat types are provided as follows:

  • Formation rule for weak and strict flat types:
Ξ,Γ|()AtypeΞ|ΓAtypeform\frac{\Xi, \Gamma \vert () \vdash A \; \mathrm{type}}{\Xi \vert \Gamma \vdash \flat A \; \mathrm{type}}\flat-\mathrm{form}
  • Introduction rule for weak and strict flat types:
Ξ,Γ|()a:AΞ|Γa :Aintro\frac{\Xi, \Gamma \vert () \vdash a:A}{\Xi \vert \Gamma \vdash a^\flat:\flat A}\flat-\mathrm{intro}
  • Elimination rule for weak and strict flat types:
Ξ|Γ,x:ACtypeΞ|ΓM:AΞ,u::A|ΓN:C[u /x]Ξ|Γ(letu Minn):C[M/x]elim\frac{\Xi \vert \Gamma, x:\flat A \vdash C \; \mathrm{type} \quad \Xi \vert \Gamma \vdash M:\flat A \quad \Xi, u::A \vert \Gamma \vdash N : C[u^\flat/x]}{\Xi \vert \Gamma \vdash (\mathrm{let}\; u^\flat \coloneqq M \;\mathrm{in}\; n):C[M/x]}\flat-\mathrm{elim}
  • Computation rule for weak and strict flat types respectively:
Ξ|Γ,x:ACtypeΞ|()M:AΞ,u::A|ΓN:C[u /x]Ξ|Γ(letu MinN)N[M/u]:C[M /x]compstrict\frac{\Xi \vert \Gamma, x:\flat A \vdash C \; \mathrm{type} \quad \Xi \vert () \vdash M:\flat A \quad \Xi, u::A \vert \Gamma \vdash N : C[u^\flat/x]}{\Xi \vert \Gamma \vdash (\mathrm{let}\; u^\flat \coloneqq M \;\mathrm{in}\; N) \equiv N[M/u]:C[M^\flat/x]}\flat-\mathrm{comp}\mathrm{strict}
Ξ|Γ,x:ACtypeΞ|()M:AΞ,u::A|ΓN:C[u /x]Ξ|Γβ (M,N):(letu MinN)= C[M /x]N[M/u]compweak\frac{\Xi \vert \Gamma, x:\flat A \vdash C \; \mathrm{type} \quad \Xi \vert () \vdash M:\flat A \quad \Xi, u::A \vert \Gamma \vdash N : C[u^\flat/x]}{\Xi \vert \Gamma \vdash \beta_{\flat}(M, N):(\mathrm{let}\; u^\flat \coloneqq M \;\mathrm{in}\; N) =_{C[M^\flat/x]} N[M/u]}\flat-\mathrm{comp}\mathrm{weak}

Weak flat modalities are primarily used in cohesive objective type theories, while strict flat modalities are typically used in cohesive type theories with judgmental equality, 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

cohesion

tangent cohesion

differential cohesion

graded differential cohesion

singular cohesion

id id fermionic bosonic bosonic Rh rheonomic reduced infinitesimal infinitesimal & étale cohesive ʃ discrete discrete continuous * \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 flat-modality in the above sense was introduced – in the language of ( , 1 ) (\infty,1) -toposes and as part of the axioms on “cohesive ( , 1 ) (\infty,1) -toposes” – in:

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

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

Last revised on November 15, 2022 at 20:36:14. See the history of this page for a list of all contributions to it.