\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 - Raw Syntax}

\hypertarget{initiality_project__raw_syntax}{}\section*{{Initiality Project - Raw Syntax}}\label{initiality_project__raw_syntax}

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

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{variables_and_metavariables}{Variables and meta-variables}\dotfill \pageref*{variables_and_metavariables} \linebreak
\noindent\hyperlink{sorts_operators_and_constants}{Sorts, operators, and constants}\dotfill \pageref*{sorts_operators_and_constants} \linebreak
\noindent\hyperlink{raw_terms}{Raw terms}\dotfill \pageref*{raw_terms} \linebreak
\noindent\hyperlink{operators}{Operators}\dotfill \pageref*{operators} \linebreak
\noindent\hyperlink{types}{$\Pi$-types}\dotfill \pageref*{types} \linebreak
\noindent\hyperlink{others}{Others}\dotfill \pageref*{others} \linebreak
\noindent\hyperlink{structural_induction}{Structural induction}\dotfill \pageref*{structural_induction} \linebreak
\noindent\hyperlink{equivalence}{$\alpha$-equivalence}\dotfill \pageref*{equivalence} \linebreak
\noindent\hyperlink{weakening_exchange_and_contraction}{Weakening, exchange, and contraction}\dotfill \pageref*{weakening_exchange_and_contraction} \linebreak
\noindent\hyperlink{substitution}{Substitution}\dotfill \pageref*{substitution} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

Here we define the ``raw syntax'' for our type theory. These are sets whose elements are called ``raw terms'' and ``raw types''. They are obtained by putting together operations like ``$\Sigma$-types'' and ``$\lambda$-abstraction'' in a way that ``makes sense locally'' but not necessarily globally.

In traditional approaches to logic, one often defines the raw terms (or ``well-formed formulas'') as a subset of the set of all ``strings'', i.e. finite lists of elements of some ``alphabet'' set such as $\{\Sigma,\Pi,\lambda,(,),:,\dots \}$. Note that parentheses, colons, commas, and so on are all symbols in the alphabet. In addition, this point of view requires us to alter some of the clauses to include extra parentheses, e.g. we have to write $(A\times B)$ so that $((A\times B)\times C)$ has an unambiguous meaning.

However, a more modern perspective is to regard this as defining an [[inductive type]] (in the metatheory), with each clause as a constructor. In this case, the raw terms themselves are not lists of symbols with some property, but rather \emph{trees} whose nodes are labeled with appropriate symbols. This way we obtain automatically an induction principle for defining functions by recursion and proving theorems by induction over the set of terms, which in the strings-of-symbols approach one has to prove by hand. The strings of symbols we write on the page like $(A\times B)\times C$ are then regarded as just a \emph{notation} for these ``abstract syntax trees''.

It's true that to be completely precise about the \emph{entire} passage from ``mathematics written on the page'' to its meaning, one would want to also define the strings of symbols and prove that they faithfully represent the syntax trees. This is analogous to how a compiler for a programming language must start out by ``parsing'' and ``lexing'' the code written by the programmer (which is a string of symbols) into an internal ``abstract syntax tree'' representation. However, such things are well-understood and extremely uninteresting, so much so that programmers often use ``parser generator'' programs to \emph{write parsers for them}; the interesting and nontrivial mathematics starts once we have an abstract syntax tree.

\hypertarget{variables_and_metavariables}{}\subsection*{{Variables and meta-variables}}\label{variables_and_metavariables}

Experts will know that there are many ways to deal with variable binding in type theory, including ``named variables'', ``de Bruijn indices'', ``de Bruijn levels'', ``locally nameless variables'', and so on. We will use ``named variables''. The reason is that our goal is expositional and sociological, and named variables keep the syntax as close as possible to what ``users'' of type theory are familiar with (e.g. with named variables we write $\lambda x. \lambda y. App(x,y)$, whereas with de Bruijn indices one has to write instead $\lambda. \lambda. App(2,1)$). Since we are humans writing for humans to read, we don't want to deal explicitly with de Bruijn indices, and neither do we want to pretend that we are using de Bruijn indices when we aren't \emph{really} using them.

Thus, we suppose given an infinite set $Var$, whose elements we call \emph{variables}. [[constructive mathematics|Constructivists]] should assume that $Var$ has [[decidable equality]]. In addition we assume given an operation $fr : Var \times P_{fin}(Var) \to Var$ which replaces a variable with another one that is ``fresh for'', i.e. distinct from all of, a given finite set of variables. That is, we assume that $fr(x,V) \notin V$. We also assume for simplicity that if already $x\notin V$ then $fr(x,V) = x$. We will also write $fr(x,V)$ as $x^{[V]}$, and if $X = \{x_1,\dots,x_n\}$ is a linearly ordered set of variables we will write

\begin{displaymath}
X^{[V]} = \{ x_1^{[V]}, x_2^{[V\cup \{x_1^{[V]}\}]}, \dots, x_n^{[V \cup \{x_1,\dots,x_{n-1}\}^{[V]}]}\}
\end{displaymath}
for the result of freshening each element of $X$ in succession, ensuring that they remain distinct not only from $V$ but also from each other.

We will also frequently use \emph{meta-variables}. These are simply ordinary mathematical variables in the ``metatheory'', i.e. the ordinary informal mathematics we are using in which to define and prove things about type theory. Single upper-case roman letters will usually be meta-variables ranging over raw terms or raw types. Single lower-case roman letters will usually be meta-variables ranging over variables (i.e. elements of $Var$).

\hypertarget{sorts_operators_and_constants}{}\subsection*{{Sorts, operators, and constants}}\label{sorts_operators_and_constants}

Overall, we are not attempting in this project to treat ``all type theories'' at any level of generality, instead simply dealing with individual type formers one by one (though attempting to be as ``modular'' as possible). However, at the level of \emph{raw} syntax we can easily be fully general, thereby saving ourselves some additional work in each case. Thus, we will work with a variant of what in [[Practical Foundations for Programming Languages]] are called \emph{abstract binding trees}, parametrized by a set of \emph{sorts} and a set of \emph{operators}.

For us the set of \textbf{sorts} is $Sort = \{ tm, ty \}$. That is, there are two classes of raw syntactic objects: raw terms and raw types. The only function of the notion of ``sort'' is to avoid writing exactly the same things twice in the two cases.

The set of \textbf{operators} $Op$ is a parameter of the theory; the rules for each type former begin by specifying some relevant operators. For instance, the operators associated to $\Pi$-types are $\{ \Pi, \lambda, App\}$.

Each operator is furthermore associated with a \textbf{signature} or \textbf{generalized arity}, which consists of:

\begin{enumerate}%
\item A sort (i.e. either $tm$ or $ty$).
\item A natural number $n$, the \textbf{argument arity}.
\item A [[function]] from $[n]=\{1,\dots,n\}$ to $Sort$, the \textbf{argument sorts}.
\item A natural number $m$, the \textbf{binding arity}.
\item A decidable [[relation]] $\lhd$ between $[n]$ and $[m]$ called \textbf{scoping}. If $j\lhd k$ we say that the $j^{th}$ argument is \emph{in the scope of} the $k^{th}$ binder.

\end{enumerate}
Often (e.g. in [[PFPL]]) the scoping relation is a [[function]] from $[m]$ to $[n]$, i.e. each binder has exactly one subterm in its scope. However, it is convenient to be more general; e.g. in a fully-annotated $\lambda$-abstraction $\lambda(x:A.B).M$ it is natural to consider $B$ and $M$ to be both in the scope of the variable $x$, rather than requiring this to be desugared to a form such as $\lambda(A,x.B,x'.M)$ in which potentially-different variables are bound in $B$ and $M$. Thus, we will represent $\lambda$ as an operator with 3 arguments, two of sort $ty$ and one of sort $tm$, with binding arity 1, and scoping relations $2\lhd 1$ and $3\lhd 1$.

Fully general abstract binding trees also allow each \emph{binder} to be associated to a sort. However, in our type theories all variables will range only over terms (not types).

Finally, in addition to the operators arising from type formers, we assume a collection of \textbf{constants}, each of which is an operator with binding arity $0$ and all arguments having sort $tm$.

We will usually use single upper-case typewriter font letters like $\mathtt{C},\mathtt{D}$ for meta-variables ranging over operators, including constants.

\hypertarget{raw_terms}{}\subsection*{{Raw terms}}\label{raw_terms}

Our raw syntax, though untyped, will be \emph{strongly scoped}. By this we mean that each raw term or type is indexed by a finite set of variables that may occur in it freely. To be precise, we define inductively a family of sets $Raw$ indexed by $P_{fin}(Var) \times Sort$; we call their elements \textbf{raw terms/types with variables from $V$}. Since we are in such generality, there are only two constructors of this inductive family:

\begin{itemize}%
\item For any $V\in P_{fin}(Var)$ and any $x\in V$, we have $x\in Raw(V,tm)$.


\item Suppose $\mathtt{C}$ is an operator of sort $s$, argument arity $n$ and binding arity $m$. Suppose also $V, X\in P_{fin}(Var)$, with $V\cap X = \emptyset$, ${|X|} = m$, and $X = \{x_1,\dots, x_m\}$ totally ordered. Given $j\in [n]$, write $X_j = \{x_k \mid j \lhd k \}$ for the variables bound in argument $j$, and suppose furthermore that for each $j\in [n]$ we have $M_j\in Raw(V\cup X_j, t_j)$, where $t:[n] \to Sort$ gives the argument sorts of $\mathtt{C}$. Then we have an element $\mathtt{C}(X;\vec{M}) \in Raw(V,s)$.



\end{itemize}
This can be read as saying that each set $Raw(V,s)$ consists of well-founded rooted trees containing nodes of two kinds:

\begin{itemize}%
\item Nodes labeled by a variable (element of $Var$) that is either in $V$ or is bound in some parent of that node and scopes over that node. Such a node has no children and is of sort $tm$.


\item Nodes labeled by an operator and a list of variables of its binding arity that are \emph{not} in $V$ or bound in some parent of that node. Such a node has a number of children equal to the argument arity of its operator label, of appropriate sorts, and each of its variables scopes over the subtrees of those children specified by the scoping relation of its operator label, while its sort is that of its operator label.



\end{itemize}
The above clauses also introduce notation for these trees: we will write simply ``$x$'' for the tree consisting of a single variable node with associated variable $x$, and $\mathtt{C}(X;\vec{M})$ for the tree whose root is an operator node with associated operator $\mathtt{C}$, bound variables $X$, and subtrees $\vec{M}$. (These are the ``linear'' syntaxes that have to be ``parsed'' into an abstract syntax tree if implementing type theory on a computer.) For instance, a fully annotated abstraction $\lambda(x:A.B).M$ is desugared as $\lambda(x;A,B,M)$, a node labeled by $\lambda$ and $x$ with three subtrees, two of which are in the scope of $x$.

The requirement that $V\cap X= \emptyset$ amounts to a ``local [[Barendregt convention]]'' that the names of bound variables can never clash with (or ``shadow'') any free variables, where the set of ``free variables'' is \emph{declared} for each raw term or type (the set $V$) rather than extracted by syntactic analysis. Maintaining this convention requires ``freshening'' when we weaken by adding new unused free variables; see below.

\hypertarget{operators}{}\subsection*{{Operators}}\label{operators}

For each type former, we describe its binding arity, argument arity and sorts, and scoping relation in a hopefully more readable form, by giving arbitrary names to its bound variables and arguments. We also give the ``sugared'' or ``traditional'' syntax that we will usually use for it.

For instance, the $\lambda$ row below means that $\lambda$ is an operator of sort $tm$, it has two arguments of sort $ty$ and one of sort $tm$, and one binder that scopes over the second type argument and the term argument.

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

[[!include Initiality Project - Raw Syntax - Pi-types]]

\hypertarget{others}{}\subsubsection*{{Others}}\label{others}

to be added later\ldots{}

\hypertarget{structural_induction}{}\subsection*{{Structural induction}}\label{structural_induction}

The principle of structural induction on raw terms and types says that to prove something about all of them, it suffices to consider raw terms and types constructed according to each of the above clauses (i.e. consider all possible labels for the root of an abstract syntax tree), assuming as an inductive hypothesis that the desired statement holds of all subtrees. This is a basic property of an inductive type; if our metatheory is set-theoretic then it can be proven from the definition of well-founded tree.

Similarly, there is a structural recursion principle for defining pairs of functions with domains $RawTm$ and $RawTy$: to define such a function it suffices to say, for each inductive clause, how to construct the value of the function on a tree with that root, assuming given its values on all the subtrees.

\hypertarget{equivalence}{}\subsection*{{$\alpha$-equivalence}}\label{equivalence}

We want to identify raw terms and types that differ only according to a renaming of bound variables. However, in defining this inductively, we end up having to also rename \emph{free} variables in the terms where the variables are bound. We do this all together by defining a relation $M \sim_\rho M'$, where $M\in Raw(V,s)$, $M'\in Raw(V',s)$, and $\rho$ is a bijection $V\cong V'$, by recursion on $M$ and $M'$ as follows:

\begin{itemize}%
\item If $x\in V$ and $y\in V'$, then $x \sim_\rho y$ if and only if $\rho(x)=y$.


\item For ordered sets $X,X'$ of the same cardinality, let $\xi:X\cong X'$ be the unique order-preserving bijection between them, and with $X_j = \{x_k \mid j \lhd k \}$ and $X'_j = \{x'_k \mid j \lhd k \}$ as before we have similarly $\xi_j : X_j \cong X'_j$. Then $\mathtt{C}(X;\vec{M}) \sim_{\rho} \mathtt{C}(X';\vec{M'})$ if and only if $M_j \sim_{\rho \cup \xi_j} M'_j$ for all $j$.


\item In all other cases (e.g. one of $M$ and $M'$ is a variable and the other is an operator, or they are distinct operators), $M\sim_\rho M'$ is false.



\end{itemize}
It is easy to prove by induction that:

\begin{itemize}%
\item For any $M\in Raw(V,s)$ we have $M\sim_{id} M$.
\item If $M\sim_\rho M'$ then $M' \sim_{\rho^{-1}} M$.
\item If $M\sim_\rho M'$ and $M' \sim_{\rho'} M''$, then $M\sim_{\rho'\circ\rho} M''$.

\end{itemize}
In particular, each $\sim_{id}$ is an equivalence relation on $Raw(V,s)$.

\hypertarget{weakening_exchange_and_contraction}{}\subsection*{{Weakening, exchange, and contraction}}\label{weakening_exchange_and_contraction}

For any function $\sigma :V\to W$, we define a function $Raw(V,s) \to Raw(W,s)$, written $M \mapsto M[\sigma]$, by induction on $M$. When $\sigma$ is a subset inclusion, this is ``weakening'': adding a new unused free variable. But to define weakening inductively, we will need to involve $M[\sigma]$ when $\sigma$ is an injection that is not a subset inclusion, and it is no extra trouble to define it for any function $\sigma$ at all.

\begin{itemize}%
\item If $M=x\in V$, we define $x[\sigma] = \sigma(x)$.


\item If $M=\mathtt{C}(X;\vec{M})$, we would like to define $M[\sigma]$ to be ``$\mathtt{C}(X;\vec{N})$'' where $N_j = M_j[\sigma]$. But this is not allowed by our definitions, since $X$ may not be disjoint from $W$ (though it is disjoint from $V$). Thus, recall that we have the successive freshening $X^{[W]}$ that is disjoint from $W$ and an order-preserving bijection $\xi :X \cong X^{[W]}$. Let $\xi_j:X_j \cong X^{[W]}_j$ be the restriction of $\xi$ to the variables bound in argument $j$; then recursively we have $M_j[\sigma\cup \xi_j] \in Raw(W\cup X^{[W]}_j,s_j)$. If we write $N_j = M_j[\sigma\cup \xi_j]$, then we can define $\mathtt{C}(X;\vec{M})[\sigma] = \mathtt{C}(X^{[W]};\vec{N})$.



\end{itemize}
It is easy to prove by induction that if $\rho,\rho'$ are bijections and $\rho' \circ \sigma = \sigma'\circ \rho$, then $M\sim_\rho M'$ implies $M[\sigma] \sim_{\rho'} M'[\sigma']$. That is, the structural rules respect $\alpha$-equivalence.

\hypertarget{substitution}{}\subsection*{{Substitution}}\label{substitution}

Let $N\in Raw(V,tm)$ and $M\in Raw(V\cup \{x\},s)$ where $x\notin V$; we want to define $M[N/x] \in Raw(V,s)$ by induction on $M$.

\begin{itemize}%
\item If $M=x$, then $x[N/x] = N$; this is well-typed since in this case $s=tm$.


\item If $M=y$ for some variable $y\in V$, then $y[N/x] = y$.


\item If $M = \mathtt{C}(X;\vec{M})$, we want to recursively substitute $N$ for $x$ in each $M_j$. But recall that $M_j \in Raw(V\cup \{x\} \cup X_j,s_j)$, so in order to write ``$M_j[N_j/x]$'' we need $N_j \in Raw(V\cup X_j,tm)$, whereas we are given only $N\in Raw(V,tm)$. Thus, we define $N_j = N[\sigma_j]$, where $\sigma_j:V\to V\cup X_j$ is the obvious inclusion. Then we can define $P_j = M_j[N[\sigma_j]/x]$ and hence $M[N/x] = \mathtt{C}(X;\vec{P})$.



\end{itemize}
Note that substitution is automatically ``capture-avoiding'' because of our ``strong scoping'' and local Barendregt convention. Before we can write $M[N/x]$, strong scoping requires $M$ and $N$ to have the same free variables (except for $x$, which only $M$ has), and no bound variables in $M$ can coincide with these free variables; thus no free variables in $N$ can get ``captured'' when it is substituted under binders in $M$. If $M$ and $N$ are not ``given'' with the same free variables, we need to explicitly weaken them first in order to substitute, and the definition of weakening was forced by strong scoping to rename all bound variables to keep them distinct from the newly added free ones; in particular, the bound variables in $M$ must get renamed to differ from any free variables in $N$. Finally, the definition of substitution is also forced by strong scoping to rename \emph{bound} variables in $N$ (using the weakening $[\sigma_j]$) to keep them distinct from any bound variables in $M$ under which they are substituted, ensuring that $M[N/x]$ still satisfies the Barendregt convention.

category: Initiality Project



\end{document}