The sharp 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.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 that
we postulate as a right adjoint to the
flat modality.
In this file, we postulate that ♯
is a
modal operator with a
crisp elimination principle and a
modal induction principle.
- In the file about sharp codiscrete types, we currently 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 that they are likely to change in the future.
Postulates
postulate ♯ : {l : Level} (A : UU l) → UU l unit-sharp : {l : Level} {A : UU l} → A → ♯ A sharp : {l : Level} (A : UU l) → UU l sharp = ♯
Crisp elimination for the sharp modality
Given a crisp element x :: ♯ A
we recover an element of A
. We postulate that
this construction is a crisp
coherent inverse to the sharp
unit.
postulate crisp-elim-sharp : {@♭ l : Level} {@♭ A : UU l} → @♭ ♯ A → A compute-crisp-elim-sharp : {@♭ l : Level} {@♭ A : UU l} (@♭ x : A) → crisp-elim-sharp (unit-sharp x) = x uniqueness-crisp-elim-sharp : {@♭ l : Level} {@♭ A : UU l} (@♭ x : ♯ A) → unit-sharp (crisp-elim-sharp x) = x coherence-uniqueness-crisp-elim-sharp : {@♭ l : Level} {@♭ A : UU l} (@♭ x : A) → ( uniqueness-crisp-elim-sharp (unit-sharp x)) = ( ap unit-sharp (compute-crisp-elim-sharp x))
Rewriting. In the future we may enable rewrite rules for the computation and uniqueness property of the crisp elimination principle for the sharp modality.
{-# REWRITE compute-crisp-elim-sharp uniqueness-crisp-elim-sharp #-}
Crisp induction for the sharp modality
The crisp induction principle¶ for the sharp modality is a crisp version of the principle that sharp codiscrete types are local at the flat counit.
postulate crisp-ind-sharp : {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} (C : A → UU l2) → ((@♭ x : A) → C x) → (x : A) → ♯ (C x) compute-crisp-ind-sharp : {@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} (C : A → UU l2) (f : (@♭ x : A) → C x) → (@♭ x : A) → crisp-ind-sharp C f x = unit-sharp (f x)
Rewriting. In the future, we may enable a rewriting for the computation rule of the crisp induction principle for the sharp modality.
{-# REWRITE compute-crisp-ind-sharp #-}
Modal induction for the sharp modality
We postulate that sharp satisfies a modal induction principle below.
Note. It should also be possible to construct it from the more general
pointwise-sharp
considered below, but we leave this for future work.
postulate 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
The sharp modality's action on "pointwise" type families
TODO. This section consists entirely of unfinished work that is not typechecked as part of the library. This code is included as notes for future work.
postulate
pointwise-sharp :
{@♭ l1 : Level} {l2 : Level} {@♭ A : UU l1} → (@♭ A → UU l2) → A → UU l2
postulate
unit-pointwise-sharp :
{@♭ l1 : Level} {@♭ A : UU l1} {l2 : Level}
{B : @♭ A → UU l2} (a : (@♭ x : A) → B x) →
(x : A) → pointwise-sharp B x
elim-pointwise-sharp :
{@♭ l1 l2 : Level} {@♭ A : UU l1} {B : @♭ A → UU l2}
(f : (@♭ x : A) → pointwise-sharp B x) → (@♭ x : A) → B x
compute-pointwise-sharp :
{@♭ l1 : Level} {@♭ A : UU l1} {l2 : Level}
(B : A → UU l2) (x : A) → pointwise-sharp (λ a → B a) x = ♯ (B x)
{-# REWRITE compute-pointwise-sharp #-}
compute-unit-pointwise-sharp :
{@♭ l1 : Level} {@♭ A : UU l1} {l2 : Level}
{B : @♭ A → UU l2} (f : (@♭ x : A) → B x)
(@♭ x : A) → unit-pointwise-sharp f x = unit-sharp (f x)
-- {-# REWRITE compute-unit-pointwise-sharp #-}
syntax elim-pointwise-sharp (λ γ → a) ctx = let♯ γ ::= ctx in♯ a ↓↓♯
Warning: When normalizing λ B x → unit-pointwise-sharp f x
, the rewrite
compute-unit-pointwise-sharp
will fire turning it into unit-sharp (f x)
,
which is ill-typed on cohesive x : A
(and the typechecker complains).
[Mey] (May be outdated info)
postulate
compute-elim-pointwise-sharp :
{@♭ l1 l2 : Level} {@♭ A : UU l1} {@♭ B : @♭ A → UU l2}
(@♭ f : (@♭ x : A) → pointwise-sharp B x)
(@♭ x : A) → elim-pointwise-sharp f x = crisp-elim-sharp (f x)
{-# REWRITE compute-elim-pointwise-sharp #-}
Uncrispening contexts
record
context-uncrisp-sharp
{@♭ l1 l2 : Level} {@♭ A : UU l1} : UU (lsuc (l1 ⊔ l2))
where
constructor ctx
field
ᶜB : A → UU l2
ᶜf : (@♭ x : A) → ♯ (ᶜB x)
ᶜa : A
open context-uncrisp-sharp
module _
{@♭ l1 l2 : Level} {@♭ A : UU l1}
where
uncrisp-sharp : (B : A → UU l2) (f : (@♭ x : A) → ♯ (B x)) → (x : A) → ♯ (B x)
uncrisp-sharp B f x =
unit-pointwise-sharp (λ γ → crisp-elim-sharp ((ᶜf γ) (ᶜa γ))) (ctx B f x)
compute-uncrisp-sharp :
(@♭ B : A → UU l2) (@♭ f : (@♭ x : A) → ♯ (B x)) (@♭ x : A) →
uncrisp-sharp B f x = f x
compute-uncrisp-sharp B f x =
compute-unit-pointwise-sharp
( λ γ → crisp-elim-sharp ((ᶜf γ) (ᶜa γ)))
( ctx B f x)
module _
{@♭ l1 l2 l3 : Level}
{@♭ A : UU l1} {@♭ B : A → UU l2}
where
uncrisp-sharp² :
(C : (x : A) → B x → UU l3)
(f : (@♭ x : A) (@♭ y : B x) → ♯ (C x y))
(x : A) (y : B x) → ♯ (C x y)
uncrisp-sharp² C f x y =
uncrisp-sharp (λ (x , y) → C x y) (λ p → f (pr1 p) (pr2 p)) (x , y)
compute-uncrisp-sharp² :
(@♭ C : (x : A) → B x → UU l3)
(@♭ f : (@♭ x : A) (@♭ y : B x) → ♯ (C x y))
(@♭ x : A) (@♭ y : B x) → uncrisp-sharp² C f x y = f x y
compute-uncrisp-sharp² C f x y =
compute-uncrisp-sharp (λ (x , y) → C x y) (λ p → f (pr1 p) (pr2 p)) (x , y)
Sharp induction revisited
The following definitions rely on rewrite rules.
module _
{@♭ l1 l2 : Level} {@♭ A : UU l1} (@♭ C : ♯ A → UU l2)
(@♭ f : (x : A) → ♯ (C (unit-sharp x)))
where
ind-sharp' : (x : ♯ A) → ♯ (C x)
ind-sharp' =
crisp-ind-sharp C (λ x → crisp-elim-sharp (f (crisp-elim-sharp x)))
compute-ind-sharp' : (@♭ x : A) → ind-sharp' (unit-sharp x) = f x
compute-ind-sharp' x =
compute-crisp-ind-sharp C
( λ x → crisp-elim-sharp (f (crisp-elim-sharp x)))
( unit-sharp x)
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) = ♯ pr2 (sharp-locally-small-operator-modality l) A = is-locally-small' {l} {♯ A}
The sharp modality's 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)
The sharp modality's recursion principle
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)
References
- [Che]
- Felix Cherubini. Felixwellen/DCHoTT-Agda. GitHub repository. URL: https://github.com/felixwellen/DCHoTT-Agda.
- [Lic]
- Dan Licata. Dlicata335/cohesion-agda. GitHub repository. URL: https://github.com/dlicata335/cohesion-agda.
- [Mey]
- David Jaz Meyers. Davidjaz/cohesion. GitHub repository. URL: https://github.com/DavidJaz/Cohesion.
- [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.
External links
- sharp modality at Lab
Recent changes
- 2024-09-23. Fredrik Bakke. Some typos, wording improvements, and brief prose additions (#1186).
- 2024-09-06. Fredrik Bakke. Basic properties of the flat modality (#1078).
- 2024-03-12. Fredrik Bakke. Bibliographies (#1058).
- 2023-11-24. Fredrik Bakke. Modal type theory (#701).