Flat Modality

The flat/crisp attribute @♭/@flat is an idempotent comonadic modality modeled after Spatial Type Theory and Crisp Type Theory. It is similar to a necessity modality.

We can define A as a type for any (@♭ A : Set l) via an inductive definition:

data{@♭ l : Level} (@♭ A : Set l) : Set l where
  con : (@♭ x : A)  ♭ A

counit : {@♭ l : Level} {@♭ A : Set l}  ♭ A  A
counit (con x) = x

When trying to provide a @♭ arguments only other @♭ variables will be available, the others will be marked as @⊤ in the context. For example the following will not typecheck:

unit : {@♭ l : Level} {@♭ A : Set l}  A  ♭ A
unit x = con x

Pattern Matching on @♭

Agda allows matching on @♭ arguments by default. When matching on a @♭ argument the flat status gets propagated to the arguments of the constructor

data _⊎_ (A B : Set) : Set where
  inl : A  A ⊎ B
  inr : B  A ⊎ B

flat-sum : {@♭ A B : Set}  (@♭ x : A ⊎ B)  ♭ A ⊎ ♭ B
flat-sum (inl x) = inl (con x)
flat-sum (inr x) = inr (con x)

When refining @♭ variables the equality also needs to be provided as @♭

flat-subst : {@♭ A : Set} {P : A  Set} (@♭ x y : A) (@♭ eq : x ≡ y)  P x  P y
flat-subst x .x refl p = p

if we simply had (eq : x y) the code would be rejected.

Pattern matching on @♭ arguments can be disabled entirely by using the --no-flat-split flag

{-# OPTIONS --no-flat-split #-}

Subtyping of flat function spaces

Normally, if f : (@♭ x : A) B then we have λ x f x : (x : A) B but not f : (x : A) B. When the option --subtyping is enabled, Agda will make use of the subtyping rule (@♭ x : A) B <: (x : A) B, so there is no need for eta-expanding the function f.