The sharp 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.sharp-modality where
Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.locally-small-types
open import foundation.universe-levels

open import orthogonal-factorization-systems.locally-small-modal-operators
open import orthogonal-factorization-systems.modal-induction
open import orthogonal-factorization-systems.modal-subuniverse-induction

Idea

The sharp modality is an axiomatized monadic modality we postulate as a right adjoint to the flat modality.

In this file, we only postulate that is a modal operator that has a modal induction principle. In the file about codiscrete types, we postulate that the subuniverse of sharp modal types has appropriate closure properties. In the flat-sharp adjunction, we postulate that it has the appropriate relation to the flat modality, making it a lex modality. Please note that there is some redundancy between the postulated axioms, and they may be subject to change in the future.

Postulates

postulate
   : {l : Level} (A : UU l)  UU l

  @unit-sharp : {l : Level} {A : UU l}  A   A

  ind-sharp :
    {l1 l2 : Level} {A : UU l1} (C :  A  UU l2) 
    ((x : A)   (C (unit-sharp x))) 
    ((x :  A)   (C x))

  compute-ind-sharp :
    {l1 l2 : Level} {A : UU l1} (C :  A  UU l2)
    (f : (x : A)   (C (unit-sharp x))) 
    (ind-sharp C f  unit-sharp) ~ f

Definitions

The sharp modal operator

sharp-locally-small-operator-modality :
  (l : Level)  locally-small-operator-modality l l l
pr1 (sharp-locally-small-operator-modality l) =  {l}
pr2 (sharp-locally-small-operator-modality l) A = is-locally-small' {l} { A}

The sharp induction principle

induction-principle-sharp :
  {l : Level}  induction-principle-modality {l} unit-sharp
pr1 (induction-principle-sharp P) = ind-sharp P
pr2 (induction-principle-sharp P) = compute-ind-sharp P

strong-induction-principle-subuniverse-sharp :
  {l : Level}  strong-induction-principle-subuniverse-modality {l} unit-sharp
strong-induction-principle-subuniverse-sharp =
  strong-induction-principle-subuniverse-induction-principle-modality
    ( unit-sharp)
    ( induction-principle-sharp)

strong-ind-subuniverse-sharp :
  {l : Level}  strong-ind-subuniverse-modality {l} unit-sharp
strong-ind-subuniverse-sharp =
  strong-ind-strong-induction-principle-subuniverse-modality
    ( unit-sharp)
    ( strong-induction-principle-subuniverse-sharp)

compute-strong-ind-subuniverse-sharp :
  {l : Level} 
  compute-strong-ind-subuniverse-modality {l}
    unit-sharp
    strong-ind-subuniverse-sharp
compute-strong-ind-subuniverse-sharp =
  compute-strong-ind-strong-induction-principle-subuniverse-modality
    ( unit-sharp)
    ( strong-induction-principle-subuniverse-sharp)

induction-principle-subuniverse-sharp :
  {l : Level}  induction-principle-subuniverse-modality {l} unit-sharp
induction-principle-subuniverse-sharp =
  induction-principle-subuniverse-induction-principle-modality
    ( unit-sharp)
    ( induction-principle-sharp)

ind-subuniverse-sharp :
  {l : Level}  ind-subuniverse-modality {l} unit-sharp
ind-subuniverse-sharp =
  ind-induction-principle-subuniverse-modality
    ( unit-sharp)
    ( induction-principle-subuniverse-sharp)

compute-ind-subuniverse-sharp :
  {l : Level} 
  compute-ind-subuniverse-modality {l} unit-sharp ind-subuniverse-sharp
compute-ind-subuniverse-sharp =
  compute-ind-induction-principle-subuniverse-modality
    ( unit-sharp)
    ( induction-principle-subuniverse-sharp)

Sharp recursion

rec-sharp :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} 
  (A   B)  ( A   B)
rec-sharp {B = B} = ind-sharp  _  B)

compute-rec-sharp :
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  (f : A   B) 
  (rec-sharp f  unit-sharp) ~ f
compute-rec-sharp {B = B} = compute-ind-sharp  _  B)

recursion-principle-sharp :
  {l : Level}  recursion-principle-modality {l} unit-sharp
pr1 (recursion-principle-sharp) = rec-sharp
pr2 (recursion-principle-sharp) = compute-rec-sharp

strong-recursion-principle-subuniverse-sharp :
  {l : Level}  strong-recursion-principle-subuniverse-modality {l} unit-sharp
strong-recursion-principle-subuniverse-sharp =
  strong-recursion-principle-subuniverse-recursion-principle-modality
    ( unit-sharp)
    ( recursion-principle-sharp)

strong-rec-subuniverse-sharp :
  {l : Level}  strong-rec-subuniverse-modality {l} unit-sharp
strong-rec-subuniverse-sharp =
  strong-rec-strong-recursion-principle-subuniverse-modality
    ( unit-sharp)
    ( strong-recursion-principle-subuniverse-sharp)

compute-strong-rec-subuniverse-sharp :
  {l : Level} 
  compute-strong-rec-subuniverse-modality {l}
    unit-sharp
    strong-rec-subuniverse-sharp
compute-strong-rec-subuniverse-sharp =
  compute-strong-rec-strong-recursion-principle-subuniverse-modality
    ( unit-sharp)
    ( strong-recursion-principle-subuniverse-sharp)

recursion-principle-subuniverse-sharp :
  {l : Level}  recursion-principle-subuniverse-modality {l} unit-sharp
recursion-principle-subuniverse-sharp =
  recursion-principle-subuniverse-recursion-principle-modality
    ( unit-sharp)
    ( recursion-principle-sharp)

rec-subuniverse-sharp :
  {l : Level}  rec-subuniverse-modality {l} unit-sharp
rec-subuniverse-sharp =
  rec-recursion-principle-subuniverse-modality
    ( unit-sharp)
    ( recursion-principle-subuniverse-sharp)

compute-rec-subuniverse-sharp :
  {l : Level} 
  compute-rec-subuniverse-modality {l} unit-sharp rec-subuniverse-sharp
compute-rec-subuniverse-sharp =
  compute-rec-recursion-principle-subuniverse-modality
    ( unit-sharp)
    ( recursion-principle-subuniverse-sharp)

Action on maps

ap-sharp : {l1 l2 : Level} {A : UU l1} {B : UU l2}  (A  B)  ( A   B)
ap-sharp f = rec-sharp (unit-sharp  f)

See also

References

Recent changes