The flat modality
Content created by Fredrik Bakke.
Created on 2023-11-24.
Last modified on 2024-03-12.
{-# 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
- In the flat-sharp adjunction we postulate that the flat modality is left adjoint to the sharp modality.
- Flat discrete types for types that are flat modal.
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
- 2024-03-12. Fredrik Bakke. Bibliographies (#1058).
- 2023-11-24. Fredrik Bakke. Modal type theory (#701).