\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 - Totality}

\hypertarget{initiality_project__totality}{}\section*{{Initiality Project - Totality}}\label{initiality_project__totality}

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

\noindent\hyperlink{overview}{Overview}\dotfill \pageref*{overview} \linebreak
\noindent\hyperlink{inductive_clauses}{Inductive clauses}\dotfill \pageref*{inductive_clauses} \linebreak
\noindent\hyperlink{variables}{Variables}\dotfill \pageref*{variables} \linebreak
\noindent\hyperlink{modeswitching}{Mode-switching}\dotfill \pageref*{modeswitching} \linebreak
\noindent\hyperlink{equality}{Equality}\dotfill \pageref*{equality} \linebreak
\noindent\hyperlink{constants}{Constants}\dotfill \pageref*{constants} \linebreak
\noindent\hyperlink{types}{$\Pi$-types}\dotfill \pageref*{types} \linebreak
\noindent\hyperlink{valid_contexts}{Valid Contexts}\dotfill \pageref*{valid_contexts} \linebreak


\hypertarget{overview}{}\subsection*{{Overview}}\label{overview}

We now prove that the [[Initiality Project - Partial Interpretation|partial interpretations]] of types, terms, and contexts satisfy the following ``local'' totality properties, for any raw context $\Gamma$ with variables $V$.

\begin{enumerate}%
\item If $\Gamma \vdash A\, type$ is derivable, then the domain of $\llbracket A \rrbracket^V_{type} : Tm^V \rightharpoonup Ty$ contains $\llbracket\Gamma\rrbracket$.
\item If $\Gamma \vdash T \Rightarrow A$ is derivable, then the domain of $\llbracket T \rrbracket^V_{\Rightarrow} : Tm^V \rightharpoonup Tm$ contains $\llbracket\Gamma\rrbracket$, and the composite $Tm^V \overset{\llbracket T \rrbracket^V_{\Rightarrow}}{\rightharpoonup} Tm \to Ty$ agrees with $\llbracket A \rrbracket^V_{type}$ on $\llbracket\Gamma\rrbracket$.
\item If $\Gamma \vdash T \Leftarrow A$ is derivable, then the domain of $\llbracket T \rrbracket^V_{\Leftarrow} : Tm^V \times Ty \rightharpoonup Tm$ contains the subobject defined by $\llbracket\Gamma\rrbracket \hookrightarrow Tm^V \overset{(id,\llbracket A \rrbracket^V_{type})}{\rightharpoonup} Tm^V \times Ty$.
\item If $\Gamma \vdash A \equiv B \, type$ is derivable, then $\llbracket A \rrbracket^V_{type}$ and $\llbracket B \rrbracket^V_{type}$ agree when their domains are intersected with each other and also with $\llbracket\Gamma\rrbracket$.
\item If $\Gamma \vdash S \equiv T : A$ is derivable, then $\llbracket S \rrbracket^V_{\Leftarrow}$ and $\llbracket T \rrbracket^V_{\Leftarrow}$ agree when their domains are intersected with each other and also with the subobject $\llbracket\Gamma\rrbracket \hookrightarrow Tm^V \times Ty$ defined in (3) above.

\end{enumerate}
The proof is by mutual induction on these mutually defined inductive judgments; thus we have one clause for each primitive rule in our [[Initiality Project - Type Theory|type theory]].

\hypertarget{inductive_clauses}{}\subsection*{{Inductive clauses}}\label{inductive_clauses}

\hypertarget{variables}{}\subsubsection*{{Variables}}\label{variables}

\hypertarget{modeswitching}{}\subsubsection*{{Mode-switching}}\label{modeswitching}

\hypertarget{equality}{}\subsubsection*{{Equality}}\label{equality}

\hypertarget{constants}{}\subsubsection*{{Constants}}\label{constants}

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

include [[Initiality Project - Totality - Pi-types]]

\hypertarget{valid_contexts}{}\subsection*{{Valid Contexts}}\label{valid_contexts}

The above totality theorem is called ``local'' because it only says the interpretations are defined on the interpretation of the context; if the context is invalid then the latter interpretation could be empty. However, with the local totality theorem in hand, we can deduce a \emph{global} totality theorem for valid contexts. Note that this parallels how the notion of valid context was defined after giving the inductive definition of the judgments, and also how the partial interpretation of contexts was defined after giving the partial interpretations of types and terms.

The global totality theorem is:

\begin{utheorem}
If $\Gamma$ is a valid context, then $\llbracket \Gamma \rrbracket$ is a [[representable presheaf]].

\end{utheorem}
\begin{proof}
By induction on the length of $\Gamma$. If it is empty, then $\llbracket () \rrbracket = 1$, the terminal presheaf, which is representable as our CwF $C$ has a terminal object.

For a context extension $(\Gamma,x:A)$, by induction we have $\llbracket \Gamma \rrbracket$ representable. [[Initiality Project - Partial Interpretation|Recall]] that $\llbracket\Gamma,x:A\rrbracket$ is defined as a pullback

\begin{displaymath}
\array { \llbracket \Gamma, x:A \rrbracket & \to & Tm \\ \downarrow & & \downarrow \\ U & \to & Ty. }
\end{displaymath}
Since $Tm\to Ty$ is, by our definition of CwF, a [[representable morphism]], it will therefore suffice to show that $U$ is a representable object.

Now $U$ is by definition the intersection of $\llbracket\Gamma\rrbracket$ with the domain of $\llbracket A \rrbracket^V_{type}$. But since $(\Gamma,x:A)$ is valid, $\Gamma \vdash A \, type$ is derivable, so by the local totality theorem, the domain of $\llbracket A \rrbracket^V_{type}$ \emph{contains} $\llbracket \Gamma \rrbracket$. Thus, $U = \llbracket \Gamma \rrbracket$, which is representable by the inductive hypothesis.

\end{proof}
Furthermore, since $Tm\to Ty$ is \emph{algebraically} represented, at each step we obtain a specified representing object for $\llbracket\Gamma\rrbracket$. We henceforth abusively denote this object of $C$ also by $\llbracket\Gamma\rrbracket$.

Combining this with the local totality theorem, we can extract more traditional-looking interpretations of derivable judgments with valid contexts that are ``purely inside $C$'' rather than phrased in terms of presheaves.

\begin{itemize}%
\item If $\Gamma$ is valid and $\Gamma \vdash A\,type$ is derivable, we have (by local totality) a total morphism $\llbracket \Gamma \rrbracket \xrightarrow{\llbracket A \rrbracket^V_{type}} Ty$, hence (by the Yoneda lemma) an element of the set $Ty(\llbracket \Gamma\rrbracket)$, which we may denote $\llbracket A \rrbracket^\Gamma_{type}$.
\item If $\Gamma$ is valid and $\Gamma \vdash T \Rightarrow A$ is derivable, we have a total morphism $\llbracket \Gamma \rrbracket \xrightarrow{\llbracket A \rrbracket^V_{\Rightarrow}} Tm$, hence an element of the set $Tm(\llbracket \Gamma\rrbracket)$ which we may denote $\llbracket T \rrbracket^\Gamma_{\Rightarrow}$. By the rest of the local totality theorem for type synthesis, the underlying semantic type of this semantic term is $\llbracket A \rrbracket^\Gamma_{type}$.
\item If $\Gamma$ is valid and $\Gamma \vdash T \Leftarrow A$ is derivable, we similarly obtain an element $\llbracket T \rrbracket^\Gamma_{\Leftarrow A}$ of $Tm(\llbracket \Gamma\rrbracket)$, whose underlying semantic type is $\llbracket A \rrbracket^\Gamma_{type}$.

\end{itemize}
category: Initiality Project



\end{document}