This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Modal type theory

{-# 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