\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*{Initiality Project - Type Theory}

\hypertarget{initiality_project__type_theory}{}\section*{{Initiality Project - Type Theory}}\label{initiality_project__type_theory}

This page is part of the [[Initiality Project]].

\noindent\hyperlink{bidirectionality}{Bidirectionality}\dotfill \pageref*{bidirectionality} \linebreak
\noindent\hyperlink{contexts}{Contexts}\dotfill \pageref*{contexts} \linebreak
\noindent\hyperlink{judgements}{Judgment forms}\dotfill \pageref*{judgements} \linebreak
\noindent\hyperlink{modes_preconditions_etc}{Modes, preconditions, etc.}\dotfill \pageref*{modes_preconditions_etc} \linebreak
\noindent\hyperlink{primitive_rules}{Primitive rules}\dotfill \pageref*{primitive_rules} \linebreak
\noindent\hyperlink{structural_rules}{Structural rules}\dotfill \pageref*{structural_rules} \linebreak
\noindent\hyperlink{modeswitching_rule}{Mode-switching rule}\dotfill \pageref*{modeswitching_rule} \linebreak
\noindent\hyperlink{equality_rules}{Equality rules}\dotfill \pageref*{equality_rules} \linebreak
\noindent\hyperlink{constant_rules}{Constant rules}\dotfill \pageref*{constant_rules} \linebreak
\noindent\hyperlink{type_former_rules}{Type former rules}\dotfill \pageref*{type_former_rules} \linebreak
\noindent\hyperlink{types}{$\Pi$-types}\dotfill \pageref*{types} \linebreak
\noindent\hyperlink{valid_contexts_and_telescopes}{Valid Contexts and Telescopes}\dotfill \pageref*{valid_contexts_and_telescopes} \linebreak
\noindent\hyperlink{bidirectional_vs_unidirectional}{Bidirectional vs Unidirectional}\dotfill \pageref*{bidirectional_vs_unidirectional} \linebreak
\noindent\hyperlink{admissible_rules}{Admissible rules}\dotfill \pageref*{admissible_rules} \linebreak
\noindent\hyperlink{inversion_lemmas}{Inversion lemmas}\dotfill \pageref*{inversion_lemmas} \linebreak
\noindent\hyperlink{structural_rules_2}{Structural rules}\dotfill \pageref*{structural_rules_2} \linebreak
\noindent\hyperlink{sanity_check}{Sanity check}\dotfill \pageref*{sanity_check} \linebreak


\hypertarget{bidirectionality}{}\subsection*{{Bidirectionality}}\label{bidirectionality}

All our terms are fully annotated. For instance, we write $App^{(x:A)B}(M,N)$ rather than just $App(M,N)$. It is, at best, unclear whether any less than fully annotated syntax can be used in an initiality theorem without ``preprocessing'' that is tantamount to annotating it.

In particular, this means that given $\Gamma$ and $T$, if $\Gamma \vdash T:A$ can be derived for any value of $A$, then there is a canonical such $A$ that can be deduced syntactically, or \emph{synthesized}, from $\Gamma$ and $T$. For instance, if $App^{(x:A)B}(M,N)$ has any type, then it must have the type $B[N/x]$. On the other hand, the conversion rule

\begin{displaymath}
\frac{\Gamma \vdash T:A \qquad \Gamma \vdash A\equiv B \,type}{\Gamma \vdash T:B}
\end{displaymath}
implies that $App^{(x:A)B}(M,N)$ must also have any type that is judgmentally \emph{equal} to $B[N/x]$. But although it \emph{has} these types, there is a sense in which it ``has'' them in a different sense from the one unique one that it synthesizes. Moreover, the conversion rule is perhaps the ickiest thing to deal with in an initiality theorem, because it can be applied absolutely anywhere, over and over again, leading to many many different derivations of the same judgment that should not be distinguished semantically.

Note that since all our terms are fully annotated, all of our formation, introduction, and elimination rules can synthesize their types. However, the type annotations also tell us what types the subterms need to have (i.e. the types that must occur in the premises of the corresponding rule), in order for the term to have its canonical type. These types may not be \emph{syntactically} equal to the types synthesized by the subterms, so we need to \emph{check} subterms against the types we want. The check should succeed if and only if the subterm's synthesized type is \emph{judgmentally} equal to the one we want; and this is the only place that the conversion rule really \emph{needs} to be applied. So in the $App^{(x:A)B}(M,N)$ example, it \emph{synthesizes} only $B[N/x]$, up to syntactic equality, but it \emph{checks against} any type judgmentally equal to $B[N/x]$.

Type theorists have a standard technique for distinguishing these two situations and controlling the use of the conversion rule, known as [[bidirectional typechecking]]. Instead of one judgment $\Gamma\vdash T:A$, we have two typing judgments:

\begin{itemize}%
\item $\Gamma \vdash T \Rightarrow A$: in context $\Gamma$ the term $T$ \emph{synthesizes} the type $A$. Here $A$ is, if it exists, uniquely determined by $\Gamma$ and $T$: it is an ``output'' to their ``inputs''.
\item $\Gamma \vdash T \Leftarrow A$: in context $\Gamma$ the term $T$ \emph{checks against} the type $A$. Here $\Gamma$, $T$, and $A$ are all ``inputs'' and the only ``output'' is the truth value of whether the typecheck is valid.

\end{itemize}
Whereas unidirectional typing rules have the conversion rule, allowing the type to be changed at any point to a judgmentally equal one, with bidirectional typing rules, conversion is only used when switching from a synthesizing premise to a checking conclusion, using the ``mode-switching'' rule:

\begin{displaymath}
\frac{\Gamma \vdash T\Rightarrow A \qquad \Gamma \vdash A\equiv B \,type}{\Gamma \vdash T\Leftarrow B}
\end{displaymath}
Unlike typical versions of bidirectional typing, in our approach the checking judgment is defined \emph{solely} by the mode-switching rule, and all other typing rules conclude a synthesizing judgment. This variant doesn't help with typechecking algorithms, but it still factors out type conversion cleanly: the equality judgment is used when, and only when, the mode switches.

So in summary, terms formers are fully annotated, their typing rules \emph{synthesize} a type in the conclusion, and have premises that \emph{check} their subterms against appropriate types. So the mode-switching rule gets applied a lot, because it's the only way, in our system, to derive a checking judgment.

From a syntactic perspective, there are many advantages of bidirectional typechecking, but it is unclear at present whether any of them are relevant to categorical semantics (although by using a bidirectional framework we are better placed to take advantage of them if they do become relevant). But more importantly, the natural structure of the semantic interpretation, as suggested by [[Peter Lumsdaine]], matches the syntactic bidirectional picture quite closely, and it may be clarifying to make that analogy more precise.

Typical versions of bidirectional typing also have bidirectional \emph{equality} rules, which essentially implement an algorithm for equality-checking. (Such partially-type-directed algorithms have advantages over simply normalizing both terms and comparing normal forms, such as more easily incorporating eta-conversion.) However, since we want our theorem to generalize to type theories in which equality is not algorithmic (e.g. theories with equality reflection) --- and more importantly, since in semantic equality there is no ``output information'' to ever compute --- we will not orient our equality judgments.

Our sort of bidirectional theory is very closely related to a unidirectional theory that may be more familiar to some readers. Roughly speaking, to go from a unidirectional theory to our sort of bidirectional one: make sure everything is fully annotated, make the conclusions of formation/introduction/elimination rules synthesizing and their premises checking, and replace the conversion rule by the mode-switching rule. Oppositely, to recover a unidirectional theory from our bidirectional one, simply collapse both checking and synthesizing judgments into the ``term has a type'' judgment $T:A$, thereby generalizing the mode-switching rule to the conversion rule. Below we will make this ``isomorphism'' a bit more precise.

\hypertarget{contexts}{}\subsection*{{Contexts}}\label{contexts}

A \textbf{raw context} is a finite list of pairs consisting of a variable and a raw term in which the variables occurring are all pairwise distinct. Each such pair, written $x:A$, is called a \textbf{typing declaration}, with $A$ being a type to which the variable $x$ belongs.

A \textbf{valid context} is a raw context $(x_1:A_1, \dots ,x_n:A_n)$ such that each judgment $x_1:A_1,\dots, x_k:A_k \vdash A_{k+1} \, type$ is derivable by the rules below. This notion is defined \emph{a posteriori} after the primitive rules for all the judgments have been given. In particular, the judgments themselves never refer to context validity. The intuitive interpretation of a judgment-in-context $\Gamma\vdash \mathcal{J}$ should therefore be ``\emph{if} $\Gamma$ is a valid context, then $\mathcal{J}$ holds in that context'' (and this is the meaning we will give it semantically).

\hypertarget{judgements}{}\subsection*{{Judgment forms}}\label{judgements}

Our type theory has five judgment forms. Here $\Gamma$ is a metavariable ranging over raw contexts, while $S,T,A,B$ are metavariables ranging over raw terms.

\begin{enumerate}%
\item $\Gamma \vdash A\,type$ --- ``$A$ is a type in context $\Gamma$''.
\item $\Gamma \vdash T \Leftarrow A$ --- ``$T$ can be checked to have type $A$ in context $\Gamma$''
\item $\Gamma \vdash T \Rightarrow A$ --- ``$T$ synthesizes the type $A$ in context $\Gamma$''
\item $\Gamma \vdash A \equiv B \, type$ --- ``$A$ and $B$ are judgmentally equal types in context $\Gamma$''
\item $\Gamma \vdash S \equiv T : A$ --- ``$S$ and $T$ are judgmentally equal terms of type $A$ in context $\Gamma$''

\end{enumerate}
\hypertarget{modes_preconditions_etc}{}\subsubsection*{{Modes, preconditions, etc.}}\label{modes_preconditions_etc}

All the metavariables occurring in all of our judgments should be regarded as ``inputs'', with the sole exception that $A$ in the synthesizing judgment $\Gamma \vdash T \Rightarrow A$ is an output. In other words, if we regard ``searching for a derivation of some judgment'' as an ``algorithm'', with the rules for deriving that judgment as the ``cases to try'' and their premises as the resulting ``recursive calls'', then in all but one case the algorithm takes all the arguments of the judgment as inputs and returns only a [[truth value]], while in the exceptional case $\Gamma \vdash T \Rightarrow A$ it takes $\Gamma$ and $T$ as inputs and returns $A$ as output (if it succeeds, otherwise it returns failure).

Note, though, that because our judgmental equality is not bidirectional and need not be even semidecidable, these ``algorithms'' are not really algorithms, unless we regard the equality judgment as a sort of ``oracle'' that they can invoke.

Similarly, we regard validity of all the ``inputs'' of each judgment as something that the ``caller'' should ensure, while validity of the ``output'' as something that the function returning it should ``promise''. For example, the rules for deriving a judgment such as $\Gamma \vdash T \Leftarrow A$ need only be ``correct'' under the \emph{assumption} that $\Gamma$ is a valid context and $\Gamma \vdash A\,type$, but in turn these assumptions must ensure that all the analogous ``preconditions'' of all \emph{premises} of such rules hold.

\hypertarget{primitive_rules}{}\subsection*{{Primitive rules}}\label{primitive_rules}

\hypertarget{structural_rules}{}\subsubsection*{{Structural rules}}\label{structural_rules}

The main structural rule is the ``variable'' or ``hypothesis'' rule, which says that if a variable is declared in a context, then as a term it synthesizes the type that it is declared with:

\begin{displaymath}
\frac{(x:A) \in \Gamma}{\Gamma \vdash x \Rightarrow A}
\end{displaymath}
The other structural rules of weakening, contraction, and substitution will be admissible.

\hypertarget{modeswitching_rule}{}\subsubsection*{{Mode-switching rule}}\label{modeswitching_rule}

The mode-switching rule says that to check that a term has a given type, we first synthesize a type for that term and then check that this type equals the given one. In our fully annotated system, this is the \emph{only} way to derive the checking judgment $\Gamma \vdash T \Leftarrow B$.

\begin{displaymath}
\frac{\Gamma \vdash T \Rightarrow A \qquad \Gamma \vdash A \equiv B \, type}{\Gamma \vdash T \Leftarrow B}
\end{displaymath}
This is also the only incarnation of the conversion rule, which in a ``unidirectional'' system is

\begin{displaymath}
\frac{\Gamma \vdash T : A \qquad \Gamma \vdash A \equiv B \, type}{\Gamma \vdash T : B.}
\end{displaymath}
A bidirectional system controls this rule more carefully, enforcing it to be used (when and) only when the mode switches.

\hypertarget{equality_rules}{}\subsubsection*{{Equality rules}}\label{equality_rules}

We have primitive rules asserting that equality of terms and types are both reflexive, transitive, and symmetric, and moreover that equality of terms is invariant under equality of types.

For equality of types $\Gamma \vdash A \equiv B$, we take as input that $\Gamma \vdash A\,type$ and $\Gamma \vdash B\,type$, so we don't need any premise in the reflexivity rule, but we do need one in the transitivity rule.

[[!include Initiality Project - Type Theory - Type equality]]

Similarly $\Gamma \vdash T \equiv S : A$ takes as input that $\Gamma \vdash T \Leftarrow A$ and $\Gamma \vdash S \Leftarrow A$. It also takes $\Gamma \vdash A type$.

[[!include Initiality Project - Type Theory - Term equality]]

\hypertarget{constant_rules}{}\subsubsection*{{Constant rules}}\label{constant_rules}

TODO. In fact, specifying the constant rules is part of the ``signature''.

\hypertarget{type_former_rules}{}\subsubsection*{{Type former rules}}\label{type_former_rules}

Each type former ($\Pi$-types, $\Sigma$-types, etc.) has a collection of rules giving its

\begin{itemize}%
\item formation rule (when is it a valid type)
\item introduction rule (what terms synthesize this type)
\item elimination rule (how terms in this type can be used)
\item equality rules ([[beta-reduction]] and, sometimes, [[eta-conversion]])
\item congruence rules (the type former and its introduction and elimination forms respect judgmental equality)

\end{itemize}
\hypertarget{types}{}\subsubsection*{{$\Pi$-types}}\label{types}

[[!include Initiality Project - Type Theory - Pi-types]]

\hypertarget{valid_contexts_and_telescopes}{}\subsection*{{Valid Contexts and Telescopes}}\label{valid_contexts_and_telescopes}

A (raw) \textbf{telescope} $\Delta$ is a (raw) context. A \textbf{valid telescope} $\Gamma \vdash \Delta ok$ is defined by another inductively-defined judgment form:

\begin{displaymath}
\frac{}{\Gamma \vdash \cdot ok}
\end{displaymath}
\begin{displaymath}
\,
\end{displaymath}
\begin{displaymath}
\frac{\Gamma \vdash \Delta ok \qquad
        \Gamma,\Delta \vdash A type \qquad
        x \notin \Gamma,\Delta}
    {\Gamma \vdash \Delta,x:A ok}
\end{displaymath}
Intuitively, a telescope is an open context. So a \textbf{valid context} can now be formalized as the closed special case of a valid telescope, with the single-rule judgment form:

\begin{displaymath}
\frac{\cdot \vdash \Gamma ok}{\Gamma ok}
\end{displaymath}
A valid telescope can also be understood as a valid multi-step context extension. So we have the theorem:

($\Gamma ok$ and $\Gamma \vdash \Delta ok$) if and only if $\Gamma,\Delta ok$.

You can also concatenate telescopes:

($\Gamma \vdash \Delta ok$ and $\Gamma,\Delta \vdash \Delta' ok$) if and only if $\Gamma \vdash \Delta,\Delta' ok$.

In fact, by the definition of context validity, the multi-step context extension is a special case of telescope concatenation.

\hypertarget{bidirectional_vs_unidirectional}{}\subsection*{{Bidirectional vs Unidirectional}}\label{bidirectional_vs_unidirectional}

As noted above, there is a canonical correspondence between our bidirectional theory (with any choice of type formers) and a unidirectional one obtained by collapsing both typing judgments $T\Leftarrow A$ and $T\Rightarrow A$ into one $T:A$ (and thereby the mode-switching rule into the conversion rule).

In fact, we can prove that $\Gamma \vdash T\Leftarrow A$ is derivable bidirectionally if and only if $\Gamma \vdash T: A$ is derivable unidirectionally.

The ``only if'' direction is easy: just change all the $\Leftarrow$s and $\Rightarrow$s to colons in a bidirectional rule to obtain a unidirectional one. For ``if'', it suffices to show that all the unidirectional rules translate to \emph{admissible} bidirectional rules under $(T:A)\mapsto(T\Leftarrow A)$. Each type-former rule in fact translates to a derivable rule: follow the corresponding bidirectional rule (whose conclusion is synthesizing) by the mode-switching rule applied to reflexivity. The only thing requiring a bit of thought is the conversion rule: we want to show that

\begin{displaymath}
\frac{\Gamma \vdash T\Leftarrow A \qquad \Gamma \vdash A\equiv B \, type}{\Gamma \vdash T\Leftarrow B}
\end{displaymath}
is admissible in our bidirectional theory. But as noted above, any derivation of $\Gamma \vdash T\Leftarrow A$ must end with an invocation of the mode-switching rule. So there must be some $C$, such that $\Gamma \vdash T\Leftarrow A$ was derived by

\begin{displaymath}
\frac{\Gamma \vdash T\Rightarrow C \qquad \Gamma \vdash C\equiv A \, type}{\Gamma \vdash T\Leftarrow A.}
\end{displaymath}
So the premises of that rule instance must be derivable. Thus, we can combine the derivations of $\Gamma \vdash C\equiv A \, type$ and $\Gamma \vdash A\equiv B \, type$ with transitivity, then apply the mode-switching rule

\begin{displaymath}
\frac{\Gamma \vdash T\Rightarrow C \qquad \Gamma \vdash C\equiv B \, type}{\Gamma \vdash T\Leftarrow B}
\end{displaymath}
to get a derivation of $\Gamma \vdash T\Leftarrow B$ as desired.

\hypertarget{admissible_rules}{}\subsection*{{Admissible rules}}\label{admissible_rules}

\hypertarget{inversion_lemmas}{}\subsubsection*{{Inversion lemmas}}\label{inversion_lemmas}

Inversion lemmas let you ``take apart'' a derivation by observing that only certain rule(s) could've been used as the last step of the derivation, based on the form of one or more objects being judged.

TODO

\hypertarget{structural_rules_2}{}\subsubsection*{{Structural rules}}\label{structural_rules_2}

Writing $\Gamma \vdash \mathcal{J}$ for one of the \hyperlink{judgements}{judgments}, the following rules are admissible by mutual induction on derivations :

\begin{displaymath}
\frac{\Gamma \vdash \Gamma' \qquad \Gamma, \Gamma' \vdash \mathcal{J}}{\Gamma, x:A, \Gamma' \vdash \mathcal{J}}
\end{displaymath}
\begin{displaymath}
\,
\end{displaymath}
\begin{displaymath}
\frac{\Gamma \vdash B\,type \qquad \Gamma, x:A, y:B, \Gamma' \vdash \mathcal{J}}{\Gamma, y:B, x:A, \Gamma' \vdash \mathcal{J}}
\end{displaymath}
\begin{displaymath}
\,
\end{displaymath}
\begin{displaymath}
\frac{\Gamma, x:A, y:A, \Gamma' \vdash \mathcal{J}}{\Gamma, x:A, \Gamma'[x/y] \vdash \mathcal{J}[x/y]}
\end{displaymath}
\begin{displaymath}
\,
\end{displaymath}
\begin{displaymath}
\frac{\Gamma \vdash T \Rightarrow A \qquad \Gamma, x:A, \Gamma' \vdash \mathcal{J}}{\Gamma, \Gamma'[T/x] \vdash \mathcal{J}[T/x]}
\end{displaymath}
(TODO)

\hypertarget{sanity_check}{}\subsubsection*{{Sanity check}}\label{sanity_check}

Sanity checks are theorems about the formal judgments that provide some confidence that the rules are propagating validity presuppositions correctly. Since we have only one judgment form that establishes any of its presuppositions, there seems to be only one sanity check we can do:

If $\Gamma ok$ and $\Gamma \vdash M \Rightarrow A$ then $\Gamma \vdash A type$.

Intuitively, a derivation $\Gamma \vdash M \Rightarrow A$ somehow contains a derivation of the presupposition $\Gamma \vdash A type$, but the derivation only makes sense when the other presupposition, $\Gamma ok$, of this judgment form, has been independently established. For example, the variable rule intuitively punts the derivation of type validity to the independent derivation of context validity.

The proof is by induction on the main derivation—of $\Gamma \vdash M \Rightarrow A$—and makes use of the admissible substitution rule:

TODO

category: Initiality Project



\end{document}