Crisp types

Content created by Fredrik Bakke.

Created on 2024-09-06.
Last modified on 2024-09-23.

module modal-type-theory.crisp-types where

Idea

In cohesive type theory, and more generally spatial type theory, one endows types with an additional structure of cohesion, as modeled by cohesive topoi and local topoi respectively. Examples include endowing types with real topological structure [Shu18] and endowing types with symmetric simplicial structure [Mye21].

One starts by introducing two modes of hypotheses: cohesive and crisp. A cohesive hypothesis is the standard mode of hypothesis. In formalizations in the agda-unimath library made outside of this module, every hypothesis may be understood to be a cohesive hypothesis. These hypotheses come with the implicit assumption that their construction is respectful of the cohesive structure of the context. Cohesive hypotheses have no restrictions on the contexts in which they may be formed.

Crisp hypotheses are, in contrast, hypotheses that are “indifferent” to the cohesive structure on types, and may only be judged in contexts made entirely out of crisp hypotheses, called crisp contexts. The indifference to cohesion is made concrete by the flat and sharp modalities.

For instance, in the framework of real-cohesive type theory, where every type is endowed with real topological structure, a cohesive variable is understood as one which varies continuously with the real topology of its type. A crisp variable on the other hand, is one that may vary discontinuously with respect to this topology.

In Agda, we state that an assumption is crisp by prepending the symbol @♭ to the hypothesis. For instance, to hypothesize two elements of an arbitrary type, one which is crisp and one which is cohesive, we may in a type signature write

  (@♭ l : Level) (@♭ A : UU l) (@♭ x : A) (y : A).

Observe that for us to be able to assume x is crisp at all, we must also assume that the type A and the universe level l are crisp, following the rule that crisp hypotheses may only be formed in crisp contexts.

So what does it mean for A to be a crisp type? Since the universe of types is itself a type, and every type comes equipped with cohesive structure, that A is a crisp type means that the definition of A is indifferent to the cohesive structure on the universe.

Note that saying a type is crisp is very different to saying that the cohesive structure of the type is trivial, which one could in one way informally state as “it consists of only crisp elements”. Crisp types whose cohesive structure is trivial in this sense is captured by flat discrete crisp types.

See also

References

[Mye21]
David Jaz Myers. Modal fracture of higher groups. 2021. arXiv:2106.15390.
[Shu18]
Michael Shulman. Brouwer's fixed-point theorem in real-cohesive homotopy type theory. Mathematical Structures in Computer Science, 28(6):856–941, 06 2018. arXiv:1509.07584, doi:10.1017/S0960129517000147.

Recent changes