\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{modal type theory} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory} [[!include type theory - contents]] \hypertarget{modalities_closure_and_reflection}{}\paragraph*{{Modalities, Closure and Reflection}}\label{modalities_closure_and_reflection} [[!include modalities - contents]] \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak \noindent\hyperlink{RelationToMonads}{Relation to monads}\dotfill \pageref*{RelationToMonads} \linebreak \noindent\hyperlink{relation_to_endoadjunctions}{Relation to endo-adjunctions}\dotfill \pageref*{relation_to_endoadjunctions} \linebreak \noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak \noindent\hyperlink{GeometricModality}{Geometric modality -- Grothendieck topology}\dotfill \pageref*{GeometricModality} \linebreak \noindent\hyperlink{closure_modality}{Closure modality}\dotfill \pageref*{closure_modality} \linebreak \noindent\hyperlink{necessity_and_possibility}{Necessity and possibility}\dotfill \pageref*{necessity_and_possibility} \linebreak \noindent\hyperlink{cohesive_and_differential_modality}{Cohesive and differential modality}\dotfill \pageref*{cohesive_and_differential_modality} \linebreak \noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak \noindent\hyperlink{References}{References}\dotfill \pageref*{References} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} \emph{Modal type theory} is a flavor of [[type theory]] with [[type formation rules]] for [[modalities]], hence [[type theory]] which on [[propositions]] reduces to [[modal logic]]. Following (\hyperlink{Moggi91}{Moggi91}, \hyperlink{BentonBiermanPaiva}{Benton-Bierman-de Paiva 95}, \hyperlink{Kobayashi}{Kobayashi 97}) modal type theory is specifically understood as being a type theory equipped with ([[comonad|co-]])[[monads]] on its type system, representing the intended [[modalities]]. Since [[monad (in computer science)|monads in computer science]] embody a notion of [[computation]], some authors also speak of \emph{[[computational type theory]]} here (\hyperlink{BentonBiermanPaiva}{Benton-Bierman-de Paiva 95}, \hyperlink{FairtloughMendler02}{Fairtlough-Mendler 02}). According to (\hyperlink{BentonBiermanPaiva}{Benton-Bierman-de Paiva 95, p. 1-2}) this matches well with the default interpretation of ([[S4]]) [[modal logic]] as being about the [[modality]] $T$ of ``[[possibility]]'': \begin{quote}% The starting point for Moggi's work is an explicit semantic distinction between \emph{computations} and \emph{values}. If $A$ is an object which interprets the values of a particular type, then $T(A)$ is the object which models computation of that type $A$. $[...]$ For a wide variety of notions of computation, the unary operator $T(-)$ turns out to have the categorical structure of a \emph{strong monad} on an underlying cartesian closed category of values. $[...]$ On a purely intuitive level and particularly if one thinks about non-termination, there is certainly something appealing about the idea that a computation of type $A$ represents the possibility of a value of type $A$. \end{quote} When the underlying type theory is [[homotopy type theory]] these modalities are a ``higher'' generalization of traditional modalities, with ``higher'' in the sense of [[higher category theory]]: they have [[categorical semantics]] in [[(∞,1)-categories]] given by [[(∞,1)-monads]]. See (\hyperlink{Shulman}{Shulman 12}, \hyperlink{RSS}{Rijke, Shulman, Spitters} ) for definition of such \emph{higher modalities}, and see at \emph{[[reflective subuniverse]]}. \hypertarget{properties}{}\subsection*{{Properties}}\label{properties} \hypertarget{RelationToMonads}{}\subsubsection*{{Relation to monads}}\label{RelationToMonads} At least in many cases, modalities in type theory are identified with [[monads (in computer science)|monads]] or comonads on the underlying [[type]] [[universe]], or on the subuniverse of [[propositions]]. See for instance (\hyperlink{BentonBiermanPaiva}{Benton-Bierman-de Paiva, section 3.2}), (\hyperlink{Kobayashi}{Kobayashi}), (\hyperlink{GabbayNanevski}{Gabbay-Nanevski, section 8}), (\hyperlink{Gaubault-LarrecqGoubault}{Gaubault-Larrecq, Goubault, section 5.1}), (\hyperlink{ParkHarper}{Park-Harper, section 2.6}), (\hyperlink{Shulman}{Shulman}) as examples of the first, and (\hyperlink{Moggi}{Moggi, def. 4.7}), (\hyperlink{AwodeyBirkedal}{Awodey-Birkedal, section 4.2}) as examples of the second. \hypertarget{relation_to_endoadjunctions}{}\subsubsection*{{Relation to endo-adjunctions}}\label{relation_to_endoadjunctions} An endo-adjunction on a [[lex category]] gives rise to a modal type theory satisfying the modal axiom K; see \hyperlink{dradjoint}{dependent right adjoint}. This also gives rise to a sound sound and complete interpretation of Fitch-style modal $\lambda$-calculus. \hypertarget{examples}{}\subsection*{{Examples}}\label{examples} \hypertarget{GeometricModality}{}\subsubsection*{{Geometric modality -- Grothendieck topology}}\label{GeometricModality} As a special case of the \hyperlink{RelationToMonads}{modalities-are-monads} relation, a [[Grothendieck topology]] on the [[site]] underlying a [[presheaf topos]] is equivalently encoded in the [[sheafification]] [[monad]] $PSh(C) \to Sh(C) \hookrightarrow PSh(C)$ induced by the [[sheaf topos]] [[geometric embedding]]. More generally, any geometric subtopos is equivalently represented by a left-exact idempotent monad. When restricted to act on [[truncated object|(-1)-truncated objects]] (i.e. [[subterminal objects]] or more generally [[monomorphisms]]), this becomes a [[universal closure operator]]. When internalized as an operation on the [[subobject classifier]], this becomes the corresponding [[Lawvere-Tierney operator]]. This modal perspective on sheafification was maybe first made explicit by [[Bill Lawvere]]: \begin{quote}% A Grothendieck `topology' appears most naturally as a modal operator of the nature `it is locally the case that' (\hyperlink{Lawvere}{Lawvere}). \end{quote} Here, ``It is locally the case that X is [[metric space\#metrizable\_spaces|metrizable]/Euclidean/etc],'' corresponds to, ``X is locally metrizable/Euclidean/etc,'' in the usual parlance. More discussion is in (\hyperlink{Goldblatt}{Goldblatt}), where this kind of modality is called a \emph{geometric modality}. For [[higher toposes]], it is no longer true in general that a subtopos is determined by its behavior on the $(-1)$-truncated objects, but we can still regard the entire sheafification monad as a [[higher modality]] in the internal [[homotopy type theory]]. \hypertarget{closure_modality}{}\subsubsection*{{Closure modality}}\label{closure_modality} The canonical monad on a [[local topos]] gives rise to a closure modality on propositions in its internal language, as described in (\hyperlink{AwodeyBirkedal}{Awodey-Birkedal}). \hypertarget{necessity_and_possibility}{}\subsubsection*{{Necessity and possibility}}\label{necessity_and_possibility} See at \emph{[[necessity and possibility]]} the section \emph{\href{https://ncatlab.org/nlab/show/necessity+and+possibility#InFirstOrderLogicAndTypeTheory}{Possible worlds via dependent type theory}} \hypertarget{cohesive_and_differential_modality}{}\subsubsection*{{Cohesive and differential modality}}\label{cohesive_and_differential_modality} By adding to [[homotopy type theory]] three (higher) modalities that encode [[discrete object|discrete types]] and [[codiscrete object|codiscrete types]] and hence implicitly a non-(co)-discrete notion of [[cohesion]] one obtained \emph{[[cohesive homotopy type theory]]}. Adding furthermore modalities for \emph{infinitesimal} (co)discreteness yields [[differential homotopy type theory]]. \hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts} \begin{itemize}% \item [[closure operator]] \item [[idempotent monad]], [[idempotent (∞,1)-monad]] \item [[modal type]], [[anti-modal type]] \item [[modal homotopy type theory]] \item [[adjoint logic]] \item [[reflective subuniverse]] \item [[geometric type theory]] \end{itemize} \hypertarget{References}{}\subsection*{{References}}\label{References} The clear identification of [[modal operators]] on types with [[monads]] (see at \emph{[[monad (in computer science)]]}) is due to \begin{itemize}% \item [[Eugenio Moggi]], \emph{Notions of computation and monads. Information and Computation}, 93(1), 1991. (\href{http://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf}{pdf}) \end{itemize} This was observed (independently) to systematically yield constructive [[modal logic]] in (see also at [[computational type theory]]) \begin{itemize}% \item P.N. Benton , G.M. Bierman , [[Valeria de Paiva]], \emph{Computational Types from a Logical Perspective I} (1995) (\href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.5778}{web}) \item M. Fairlough, Michael Mendler, \emph{Propositional lax logic}, Information and computation 137(1):1-33 (1997) \item Satoshi Kobayashi, \emph{Monad as modality}, Theoretical Computer Science, Volume 175, Issue 1, 30 (1997), Pages 29--74 \end{itemize} See also the type-theoretic generalization of \emph{[[adjoint logic]]}, as discussed in \begin{itemize}% \item [[Dan Licata]], [[Mike Shulman]], \emph{Adjoint logic with a 2-category of modes}, in \emph{\href{http://lfcs.info/lfcs-2016/}{Logical Foundations of Computer Science 2016}} (\href{http://dlicata.web.wesleyan.edu/pubs/ls15adjoint/ls15adjoint.pdf}{pdf}, \href{http://dlicata.web.wesleyan.edu/pubs/ls15adjoint/ls15adjoint-lfcs-slides.pdf}{slides}) \end{itemize} The modal systems ``CL'' and ``PLL'' in (\hyperlink{BentonBiermanPaiva}{Benton-Bierman-Paiva}) and (\hyperlink{FairloughMendler}{Fairlough-Mendler}), respectively, turn out to be equivalent to the geometric modality of \hyperlink{Goldblatt}{Goldblatt}. The system CS4 in (\hyperlink{Kobayashi}{Kobayashi}) yields a constructive version of [[S4 modal logic]]. Explicit mentioning of type theory equipped with such a monad as \emph{modal type theory} or [[computational type theory]] is in \begin{itemize}% \item Matt Fairtlough, Michael Mendler, \emph{On the Logical Content of Computational Type Theory: A Solution to Curry's Problem}, Types for Proofs and Programs Lecture Notes in Computer Science Volume 2277, 2002, pp 63-78 \end{itemize} Discussion of modal operators explicitly in [[dependent type theory]] (and with a brief mentioning of the relation to [[monad (in computer science)|monads]]) is in \begin{itemize}% \item [[Aleksandar Nanevski]], [[Frank Pfenning]], Brigitte Pientka, \emph{Contextual Modal Type Theory} (2005) (\href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.61.2356}{web}, \href{http://wips.cs.umn.edu/slides/pientka.pdf}{slides}) \item [[Valeria de Paiva]], Eike Ritter, \emph{Fibrational Modal Type Theory}, Electronic Notes in Theoretical Computer Science Volume 323, 11 July 2016, Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2015), pp. 143--161 (\href{http://www.sciencedirect.com/science/article/pii/S1571066116300378}{doi:10.1016/j.entcs.2016.06.010}) \item Daniel Gratzer, [[Jonathan Sterling]], [[Lars Birkedal]], \emph{Implementing Modal Dependent Type Theory}, (\href{https://jozefg.github.io/papers/2019-implementing-modal-dependent-type-theory.pdf}{pdf}, \href{https://github.com/jozefg/blott}{GitHub}) \item Daniel Gratzer, \emph{Implementing Modal Dependent Type Theory}, talk at \href{https://icfp19.sigplan.org/}{ICFP 19} (\href{https://jozefg.github.io/papers/2019-icfp-modal-slides.pdf}{slides pdf}) \end{itemize} A survey of the field of modal type theory is in the collections \begin{itemize}% \item M. Fairtlough, M. Mendler, [[Eugenio Moggi]] (eds.), \emph{Modalities in Type Theory}, Mathematical Structures in Computer Science, Vol. 11, No. 4, (2001) \item [[Valeria de Paiva]], Rajeev Gor\'e{}, Michael Mendler, \emph{Modalities in constructive logics and type theories}, Special issue of the Journal of Logic and Computation, editorial pp. 439-446, Vol. 14, No. 4, Oxford University Press, (2004) (\href{http://www.cs.bham.ac.uk/~vdp/publications/final-preface.pdf}{pdf}) \item [[Valeria de Paiva]], Brigitte Pientka (eds.) \emph{Intuitionistic Modal Logic and Applications (IMLA 2008)}, . Inf. Comput. 209(12): 1435-1436 (2011) (\href{http://www.sciencedirect.com/science/article/pii/S089054011100143X}{web}) \end{itemize} The historically first modal type theory, the interpretation of [[sheafification]] as a modality in the internal language of a [[Grothendieck]] topos goes back to the notion of [[Lawvere-Tierney operator]] \begin{itemize}% \item [[Bill Lawvere]], \emph{Quantifiers and sheaves}, Actes, Congr\`e{}s intern, math., 1970. Tome 1, p. 329 \`a{} 334 (\href{http://www.mathunion.org/ICM/ICM1970.1/Main/icm1970.1.0329.0334.ocr.pdf}{pdf}) \end{itemize} reviewed in \begin{itemize}% \item [[Robert Goldblatt]], \emph{Grothendieck topology as geometric modality}, Mathematical Logic Quarterly, Volume 27, Issue 31-35, pages 495--529, (1981) \end{itemize} Modal type theory with an eye towards [[homotopy type theory]] is discussed in \begin{itemize}% \item [[UF-IAS-2012]], \emph{\href{http://uf-ias-2012.wikispaces.com/Modal+type+theory}{Modal type theory}} \end{itemize} Formalization of modalities in [[homotopy type theory]] ([[modal homotopy type theory]]) is discussed in \begin{itemize}% \item [[Mike Shulman]], \emph{Higher modalities}, talk at [[UF-IAS-2012]], October 2012 (\href{http://uf-ias-2012.wikispaces.com/file/view/modalitt.pdf}{pdf}) \item [[Egbert Rijke]], [[Mike Shulman]], [[Bas Spitters]], \emph{Modalities in homotopy type theory} \href{https://arxiv.org/abs/1706.07526}{arXiv} \item [[Mike Shulman]], \emph{\href{http://homotopytypetheory.org/2015/07/05/modules-for-modalities/}{http://homotopytypetheory.org/2015/07/05/modules-for-modalities/}} (2015) \item [[Egbert Rijke]], [[Bas Spitters]], around def. 1.11 of \emph{Sets in homotopy type theory} (\href{http://arxiv.org/abs/1305.3835}{arXiv:1305.3835}) \item Kevin Quirin and Nicolas Tabareau, \emph{Lawvere-Tierney Sheafification in Homotopy Type Theory}, \href{http://hott-uf.gforge.inria.fr/2015/}{Workshop} talk 2015 (\href{http://hott-uf.gforge.inria.fr/2015/HOTTUF_Kevin.pdf}{pdf}), Kevin Quirin \href{https://kevinquirin.github.io/thesis/main.pdf}{thesis} \end{itemize} and specifically in [[cohesive homotopy type theory]] in \begin{itemize}% \item [[Urs Schreiber]], [[Michael Shulman]], \emph{[[schreiber:Quantum gauge field theory in Cohesive homotopy type theory]]}, in [[Ross Duncan]], [[Prakash Panangaden]] (eds.) \emph{Proceedings 9th Workshop on Quantum Physics and Logic}, Brussels, Belgium, 10-12 October 2012 (\href{http://arxiv.org/abs/1408.0054}{arXiv:1408.0054}) \item [[Mike Shulman]], \emph{Brouwer's fixed-point theorem in real-cohesive homotopy type theory}, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (\href{https://arxiv.org/abs/1509.07584}{arXiv:1509.07584}, \href{https://doi.org/10.1017/S0960129517000147}{doi:10.1017/S0960129517000147}) \item [[Felix Wellen]], \emph{[[schreiber:thesis Wellen|Cartan Geometry in Modal Homotopy Type Theory]]} (\href{https://arxiv.org/abs/1806.05966}{arXiv:1806.05966}, \href{http://www.math.kit.edu/iag3/~wellen/media/diss.pdf}{thesis pdf}) \end{itemize} Monadic modal type theory with [[idempotent monads]]/monadic reflection is discussed in \begin{itemize}% \item [[Andrzej Filinski]], \emph{Representing Layered Monads}, POPL 1999. (\href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.2016}{pdf}) \item [[Andrzej Filinski]], \emph{On the Relations between Monadic Semantics}, TCS 375:1-3, 2007. (\href{http://www.itu.dk/people/birkedal/teaching/advanced-semantics-Spring-2007/OtRbMS.pdf}{pdf}) \item [[Andrzej Filinski]], \emph{Monads in Action}, POPL 2010. (\href{http://camlunity.ru/swap/Library/Computer%20Science/Category%20Theory/Monads%20in%20Action.pdf}{pdf}) \item Oleg Kiselyov and Chung-chieh Shan, \emph{Embedded Probabilistic Programming. Working conference on domain-specific languages}, (2009) (\href{https://link.springer.com/content/pdf/10.1007/978-3-642-03034-5_17.pdf}{pdf}) \end{itemize} A general framework is discussed in \begin{itemize}% \item [[Dan Licata]], [[Mike Shulman]], \emph{Adjoint logic with a 2-category of modes}, in \emph{\href{http://lfcs.info/lfcs-2016/}{Logical Foundations of Computer Science 2016}} (\href{http://dlicata.web.wesleyan.edu/pubs/ls15adjoint/ls15adjoint.pdf}{pdf}, \href{http://dlicata.web.wesleyan.edu/pubs/ls15adjoint/ls15adjoint-lfcs-slides.pdf}{slides}) (for [[modal type theory|modal]] [[unary type theory]]) \item [[Daniel Licata]], [[Mike Shulman]], and [[Mitchell Riley]], \emph{A Fibrational Framework for Substructural and Modal Logics (extended version)}, in Proceedings of 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) (\href{http://drops.dagstuhl.de/opus/volltexte/2017/7740/}{doi: 10.4230/LIPIcs.FSCD.2017.25}, \href{http://dlicata.web.wesleyan.edu/pubs/lsr17multi/lsr17multi-ex.pdf}{pdf}) (for [[modal type theory|modal]] [[simple type theory]]) \end{itemize} Review includes \begin{itemize}% \item [[Dan Licata]], [[Felix Wellen]], \emph{Synthetic Mathematics in Modal Dependent Type Theories}, tutorial at \emph{\href{https://www.him.uni-bonn.de/programs/current-trimester-program/types-sets-constructions/workshop-types-homotopy-type-theory-and-verification/}{Types, Homotopy Theory and Verification}}, 2018 Tutorial 1, Dan Licata: \emph{A Fibrational Framework for Modal Simple Type Theories} (\href{https://www.youtube.com/watch?v=uLLbSAYd3yI}{recording}) Tutorial 2, Felix Wellen: \emph{The Shape Modality in Real cohesive HoTT and Covering Spaces} (\href{https://www.youtube.com/watch?v=ACGjJDarEc4}{recording}) Tutorial 3, Dan Licata: \emph{Discrete and Codiscrete Modalities in Cohesive HoTT} (\href{https://www.youtube.com/watch?v=OHN9vEVPBN8}{recording}) Tutorial 4, Felix Wellen, \emph{Discrete and Codiscrete Modalities in Cohesive HoTT, II} (\href{https://www.youtube.com/watch?v=KXx9UDQdWPw}{recording}) Tutorial 5, Dan Licata: \emph{A Fibrational Framework for Modal Dependent Type Theories} (\href{https://www.youtube.com/watch?v=R4SsxUnIcng}{recording}) Tutorial 6, Felix Wellen: \emph{Differential Cohesive HoTT}, (\href{https://www.youtube.com/watch?v=uEZXHPdwvJU&t=226s}{recording}) \item [[Dan Licata]], \emph{Synthetic Mathematics in Modal Dependent Type Theories}, notes for tutorial at \emph{\href{https://www.him.uni-bonn.de/programs/current-trimester-program/types-sets-constructions/workshop-types-homotopy-type-theory-and-verification/}{Types, Homotopy Theory and Verification}}, 2018 (\href{http://dlicata.web.wesleyan.edu/pubs/lsr17multi/him-tutorial.pdf}{pdf}) \item [[Michael Shulman]], \emph{Semantics of higher modalities}, talk at \emph{\href{http://www.andrew.cmu.edu/user/fwellen/modal-workshop.html}{Geometry in Modal HoTT (2019)}} (\href{http://home.sandiego.edu/~shulman/papers/cmu2019b.pdf}{pdf slides}, \href{https://www.youtube.com/watch?v=Wcpi1vVMrCs}{video recording}) \item [[Felix Wellen]], \emph{Geometry in Modal HoTT}, talk at \emph{\href{http://www.andrew.cmu.edu/user/fwellen/modal-workshop.html}{Geometry in Modal HoTT (2019)}} (\href{https://www.youtube.com/watch?v=oHc552-hzBY}{video recording}) \item [[Egbert Rijke]], \emph{Reflective subuniverses and modalities}, talk at \emph{\href{http://www.andrew.cmu.edu/user/fwellen/modal-workshop.html}{Geometry in Modal HoTT (2019)}} (\href{https://youtu.be/OQthe5HpiKM}{video recording}) \item [[Egbert Rijke]], \emph{Modal descent}, talk at \emph{\href{http://www.andrew.cmu.edu/user/fwellen/modal-workshop.html}{Geometry in Modal HoTT (2019)}} (\href{https://youtu.be/InaRkqKdyp4}{video recording}) \end{itemize} See also \begin{itemize}% \item [[Frank Pfenning]], \emph{Towards modal type theory} (2000) (\href{http://www.cs.cmu.edu/~fp/talks/mantova00-talk.pdf}{pdf}) \item [[Frank Pfenning]], \emph{Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory}, Pages 221--230 of: Symposium on Logic in Computer Science (2001) (\href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.5884}{web}) \item Giuseppe Primiero, \emph{A multi-modal dependent type theory} (\href{http://logica.ugent.be/centrum/preprints/primiero_PSPL10.pdf}{pdf}) \item Murdoch Gabbay, [[Aleksandar Nanevski]], \emph{Denotation of contextual modal type theory (CMTT): syntax and metaprogramming} (\href{http://www.gabbay.org.uk/papers/dencmt.pdf}{pdf}) \item G. A. Kavvos, \emph{Modalities, Cohesion, and Information Flow}, (\href{https://arxiv.org/abs/1809.07897}{arXiv:1809.07897}) \item Y. Nishiwaki, Y. Kakutani, Y. Murase, \emph{Modality via Iterated Enrichment}, MFPS 2018 (\href{https://www.mathstat.dal.ca/mfps2018/preproc/paper_15.pdf}{pdf}) \end{itemize} A modality in the [[internal language]] of a [[local topos]] is discussed in section 4.2 of \begin{itemize}% \item [[Steve Awodey]], [[Lars Birkedal]], \emph{Elementary axioms for local maps of toposes}, Journal of Pure and Applied Algebra, 177(3):215-230, (2003) (\href{http://www.itu.dk/people/birkedal/papers/elealm.ps.gz}{ps}, [[AwodeyBirkedalLocalTopos.pdf:file]] ) \item Jean Goubault-Larrecq, \'E{}ric Goubault, \emph{On the geometry of intuitionistic S4 proofs}, Homology, homotopy and applications vol 5(2) (2003) \item Sungwoo Park, [[Robert Harper]], \emph{A modal language for Effects} (2004) (\href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.8252}{web}) \item [[Dan Licata]], [[Robert Harper]], \emph{A Monadic Formalization of ML5} (\href{http://arxiv.org/abs/1009.2793}{arXiv:1009.2793}) \item Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, Bas Spitters, \emph{Modal Dependent Type Theory and Dependent Right Adjoints} \href{https://arxiv.org/abs/1804.05236}{Arxiv}, 2018 \end{itemize} A list of related references is also kept at \begin{itemize}% \item [[Valeria de Paiva]], \emph{Intuitionistic Modal Logic Selected Publications} (\href{https://docs.google.com/document/pub?id=1ASo__R-_Bzq9D9lGUo0xrfIxt_I9az7oqSg-wmP1K10}{web}) \end{itemize} [[!redirects modal type theories]] [[!redirects geometric modality]] [[!redirects geometric modalities]] [[!redirects higher modality]] [[!redirects higher modalities]] \end{document}