Modal type theory
Content created by Fredrik Bakke.
Created on 2023-11-24.
Last modified on 2023-11-24.
{-# OPTIONS --cohesion --flat-split #-}
Files in the modal type theory folder
module modal-type-theory where 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.flat-dependent-function-types public open import modal-type-theory.flat-dependent-pair-types public open import modal-type-theory.flat-discrete-types public open import modal-type-theory.flat-modality public open import modal-type-theory.flat-sharp-adjunction 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
Recent changes
- 2023-11-24. Fredrik Bakke. Modal type theory (#701).