The flat modality

Content created by Fredrik Bakke.

Created on 2023-11-24.
Last modified on 2023-11-24.

{-# 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

See also

References

Recent changes