The flat modality

Content created by Fredrik Bakke.

Created on 2023-11-24.
Last modified on 2024-09-23.

{-# OPTIONS --cohesion --flat-split #-}

module modal-type-theory.flat-modality where
Imports 
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.retractions
open import foundation.sections
open import foundation.universe-levels

Idea

The flat modality is an axiomatized comonadic modality we adjoin to our type theory by use of crisp type theory.

Definition

The flat operator on types

data ♭ {@♭ l : Level} (@♭ A : UU l) : UU l where
  intro-flat : @♭ A → ♭ A

flat : {@♭ l : Level} (@♭ A : UU l) → UU l
flat = ♭

The flat counit

counit-flat : {@♭ l : Level} {@♭ A : UU l} → ♭ A → A
counit-flat (intro-flat x) = x

Flat dependent elimination

ind-flat :
  {@♭ l1 : Level} {@♭ A : UU l1} {l2 : Level} (C : ♭ A → UU l2) →
  ((@♭ u : A) → C (intro-flat u)) →
  (x : ♭ A) → C x
ind-flat C f (intro-flat x) = f x

Flat elimination

rec-flat :
  {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} {C : UU l2} →
  (@♭ A → C) → ♭ A → C
rec-flat {C = C} = ind-flat (λ _ → C)

Crispening statements

crispen :
  {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} {P : A → UU l2} →
  ((x : A) → P x) → ((@♭ x : A) → P x)
crispen f x = f x

The associated family over ♭ A to a type family defined on crisp elements of A

family-over-flat :
  {@♭ l1 l2 : Level} {@♭ A : UU l1} (@♭ P : @♭ A → UU l2) → ♭ A → UU l2
family-over-flat P (intro-flat x) = P x

Properties

The flat modality is idempotent

module _
  {@♭ l : Level} {@♭ A : UU l}
  where

  is-crisp-section-intro-flat : (@♭ x : A) → counit-flat (intro-flat x) ＝ x
  is-crisp-section-intro-flat _ = refl

  is-crisp-retraction-intro-flat : (@♭ x : ♭ A) → intro-flat (counit-flat x) ＝ x
  is-crisp-retraction-intro-flat (intro-flat _) = refl

The equivalence ♭ A ≃ ♭ (♭ A)

module _
  {@♭ l : Level} {@♭ A : UU l}
  where

  diagonal-flat : ♭ A → ♭ (♭ A)
  diagonal-flat (intro-flat x) = intro-flat (intro-flat x)

  is-retraction-diagonal-flat : is-retraction counit-flat diagonal-flat
  is-retraction-diagonal-flat (intro-flat (intro-flat _)) = refl

  is-section-diagonal-flat : is-section counit-flat diagonal-flat
  is-section-diagonal-flat (intro-flat _) = refl

  section-diagonal-flat : section diagonal-flat
  pr1 section-diagonal-flat = counit-flat
  pr2 section-diagonal-flat = is-retraction-diagonal-flat

  retraction-diagonal-flat : retraction diagonal-flat
  pr1 retraction-diagonal-flat = counit-flat
  pr2 retraction-diagonal-flat = is-section-diagonal-flat

  abstract
    is-equiv-diagonal-flat : is-equiv diagonal-flat
    pr1 is-equiv-diagonal-flat = section-diagonal-flat
    pr2 is-equiv-diagonal-flat = retraction-diagonal-flat

  equiv-diagonal-flat : ♭ A ≃ ♭ (♭ A)
  pr1 equiv-diagonal-flat = diagonal-flat
  pr2 equiv-diagonal-flat = is-equiv-diagonal-flat

The equivalence ♭ (♭ A) ≃ ♭ A

  section-flat-counit-flat : section (counit-flat {A = ♭ A})
  pr1 section-flat-counit-flat = diagonal-flat
  pr2 section-flat-counit-flat = is-section-diagonal-flat

  retraction-flat-counit-flat : retraction (counit-flat {A = ♭ A})
  pr1 retraction-flat-counit-flat = diagonal-flat
  pr2 retraction-flat-counit-flat = is-retraction-diagonal-flat

  abstract
    is-equiv-flat-counit-flat : is-equiv (counit-flat {A = ♭ A})
    pr1 is-equiv-flat-counit-flat = section-flat-counit-flat
    pr2 is-equiv-flat-counit-flat = retraction-flat-counit-flat

  equiv-flat-counit-flat : ♭ (♭ A) ≃ ♭ A
  equiv-flat-counit-flat = inv-equiv equiv-diagonal-flat

See also

References

[Lic]
Dan Licata. Dlicata335/cohesion-agda. GitHub repository. URL: https://github.com/dlicata335/cohesion-agda.
[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