Modal type theory

Content created by Fredrik Bakke.

Created on 2023-11-24.
Last modified on 2024-09-23.

{-# OPTIONS --cohesion --flat-split #-}

Modal type theory is the study of type theory extended with syntactic modal operators. These are operations on types that increase the expressivity of the type theory in some way.

In this namespace, we consider modal extensions of Martin-Löf type theory with a flat modality ♭, sharp modality ♯, and more to come. The adjoint pair of modalities ♭ ⊣ ＃ display a structure on all types referred to as spatial, or cohesive structure.

To read more, continue to crisp types.

module modal-type-theory where

open import modal-type-theory.action-on-homotopies-flat-modality public
open import modal-type-theory.action-on-identifications-crisp-functions public
open import modal-type-theory.action-on-identifications-flat-modality public
open import modal-type-theory.crisp-cartesian-product-types public
open import modal-type-theory.crisp-coproduct-types public
open import modal-type-theory.crisp-dependent-function-types public
open import modal-type-theory.crisp-dependent-pair-types public
open import modal-type-theory.crisp-function-types public
open import modal-type-theory.crisp-identity-types public
open import modal-type-theory.crisp-law-of-excluded-middle public
open import modal-type-theory.crisp-pullbacks public
open import modal-type-theory.crisp-types public
open import modal-type-theory.dependent-universal-property-flat-discrete-crisp-types public
open import modal-type-theory.flat-discrete-crisp-types public
open import modal-type-theory.flat-modality public
open import modal-type-theory.flat-sharp-adjunction public
open import modal-type-theory.functoriality-flat-modality public
open import modal-type-theory.functoriality-sharp-modality public
open import modal-type-theory.sharp-codiscrete-maps public
open import modal-type-theory.sharp-codiscrete-types public
open import modal-type-theory.sharp-modality public
open import modal-type-theory.transport-along-crisp-identifications public
open import modal-type-theory.universal-property-flat-discrete-crisp-types public

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).
2023-11-24. Fredrik Bakke. Modal type theory (#701).

agda-unimath

Modules in the modal type theory namespace

Recent changes