This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The flat modality

{-# 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.function-types
open import foundation.homotopies
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
  cons-flat : @♭ A → ♭ A

The flat counit

counit-crisp : {@♭ l : Level} {@♭ A : UU l} → @♭ A → A
counit-crisp x = x

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

Flat dependent elimination

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

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

Flat elimination

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

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

Flat action on maps

module _
  {@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : UU l2}
  where

  ap-flat : @♭ (A → B) → (♭ A → ♭ B)
  ap-flat f (cons-flat x) = cons-flat (f x)

  ap-crisp-flat : @♭ (@♭ A → B) → (♭ A → ♭ B)
  ap-crisp-flat f (cons-flat x) = cons-flat (f x)

  coap-flat : (♭ A → ♭ B) → (@♭ A → B)
  coap-flat f x = counit-flat (f (cons-flat x))

  is-crisp-retraction-coap-flat :
    (@♭ f : @♭ A → B) → coap-flat (ap-crisp-flat f) ＝ f
  is-crisp-retraction-coap-flat _ = refl

Properties

Crisp assumptions are weaker

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

The flat modality is idempotent

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

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

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

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

  map-flat-counit-flat : ♭ (♭ A) → ♭ A
  map-flat-counit-flat (cons-flat x) = x

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

  is-section-flat-counit-flat :
    diagonal-flat ∘ map-flat-counit-flat ~ id
  is-section-flat-counit-flat (cons-flat (cons-flat _)) = refl

  is-retraction-flat-counit-flat :
    map-flat-counit-flat ∘ diagonal-flat ~ id
  is-retraction-flat-counit-flat (cons-flat _) = refl

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

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

  is-equiv-flat-counit-flat : is-equiv map-flat-counit-flat
  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
  pr1 equiv-flat-counit-flat = map-flat-counit-flat
  pr2 equiv-flat-counit-flat = is-equiv-flat-counit-flat

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

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.

agda-unimath