note.tex

\documentclass{article}

\usepackage{amssymb,amsmath,amsthm}
\usepackage{cmll}
\usepackage{stmaryrd}
\usepackage{mathpartir}
\usepackage{supertabular}
\usepackage{color}
\usepackage{fullpage}
\usepackage{verbatim}
\usepackage[textwidth=2cm]{todonotes}
\usepackage{enumitem}
\usepackage{hyperref}

\usepackage[all]{xypic}
\usepackage[barr]{xy}

%% This renames Barr's \to to \mto.  This allows us to use \to for imp
%% and \mto for a inline morphism.
\let\mto\to
\let\to\relax
\newcommand{\to}{\rightarrow}
\newcommand{\ndto}[1]{\to_{#1}}
\newcommand{\ndwedge}[1]{\wedge_{#1}}

% Commands that are useful for writing about type theory and programming language design.
%% \newcommand{\case}[4]{\text{case}\ #1\ \text{of}\ #2\text{.}#3\text{,}#2\text{.}#4}
\newcommand{\interp}[1]{\llbracket #1 \rrbracket}
\newcommand{\normto}[0]{\rightsquigarrow^{!}}
\newcommand{\join}[0]{\downarrow}
\newcommand{\redto}[0]{\rightsquigarrow}
\newcommand{\nat}[0]{\mathbb{N}}
\newcommand{\fun}[2]{\lambda #1.#2}
\newcommand{\CRI}[0]{\text{CR-Norm}}
\newcommand{\CRII}[0]{\text{CR-Pres}}
\newcommand{\CRIII}[0]{\text{CR-Prog}}
\newcommand{\subexp}[0]{\sqsubseteq}
%% Must include \usepackage{mathrsfs} for this to work.

\date{}

\let\b\relax
\let\d\relax
\let\t\relax
\let\r\relax
\let\c\relax
\let\j\relax
\let\wn\relax
\let\H\relax

% Cat commands.
\newcommand{\powerset}[1]{\mathcal{P}(#1)}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\func}[1]{\mathsf{#1}}
\newcommand{\iso}[0]{\mathsf{iso}}
\newcommand{\H}[0]{\func{H}}
\newcommand{\J}[0]{\func{J}}
\newcommand{\catop}[1]{\cat{#1}^{\mathsf{op}}}
\newcommand{\Hom}[3]{\mathsf{Hom}_{\cat{#1}}(#2,#3)}
\newcommand{\limp}[0]{\multimap}
\newcommand{\colimp}[0]{\multimapdotinv}
\newcommand{\dial}[1]{\mathsf{Dial_{#1}}(\mathsf{Sets^{op}})}
\newcommand{\dialSets}[1]{\mathsf{Dial_{#1}}(\mathsf{Sets})}
\newcommand{\dcSets}[1]{\mathsf{DC_{#1}}(\mathsf{Sets})}
\newcommand{\sets}[0]{\mathsf{Sets}}
\newcommand{\obj}[1]{\mathsf{Obj}(#1)}
\newcommand{\mor}[1]{\mathsf{Mor(#1)}}
\newcommand{\id}[0]{\mathsf{id}}
\newcommand{\lett}[0]{\mathsf{let}\,}
\newcommand{\inn}[0]{\,\mathsf{in}\,}
\newcommand{\cur}[1]{\mathsf{cur}(#1)}
\newcommand{\curi}[1]{\mathsf{cur}^{-1}(#1)}
\newcommand{\m}[1]{\mathsf{m}_{#1}}
\newcommand{\n}[1]{\mathsf{n}_{#1}}
\newcommand{\b}[1]{\mathsf{b}_{#1}}
\newcommand{\d}[1]{\mathsf{d}_{#1}}
\newcommand{\h}[1]{\mathsf{h}_{#1}}
\newcommand{\p}[1]{\mathsf{p}_{#1}}
\newcommand{\q}[1]{\mathsf{q}_{#1}}
\newcommand{\t}[0]{\mathsf{t}}
\newcommand{\r}[1]{\mathsf{r}_{#1}}
\newcommand{\s}[1]{\mathsf{s}_{#1}}
\newcommand{\w}[1]{\mathsf{w}_{#1}}
\newcommand{\c}[1]{\mathsf{c}_{#1}}
\newcommand{\j}[1]{\mathsf{j}_{#1}}
\newcommand{\jinv}[1]{\mathsf{j}^{-1}_{#1}}
\newcommand{\wn}[0]{\mathop{?}}
\newcommand{\codiag}[1]{\bigtriangledown_{#1}}

\newenvironment{changemargin}[2]{%
  \begin{list}{}{%
    \setlength{\topsep}{0pt}%
    \setlength{\leftmargin}{#1}%
    \setlength{\rightmargin}{#2}%
    \setlength{\listparindent}{\parindent}%
    \setlength{\itemindent}{\parindent}%
    \setlength{\parsep}{\parskip}%
  }%
  \item[]}{\end{list}}

\let\diagram\relax
\newenvironment{diagram}{
  \begin{center}
    \begin{math}
      \bfig
}{
      \efig
    \end{math}
  \end{center}
}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{corollary}{Corollary}[theorem]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{definition}[theorem]{Definition}

\begin{document}

\title{Notes on Fibrational Semantics of Simple, Polymorphic, and Dependent Type Theory}
\author{Harley Eades III}
\maketitle

\section{The Simple Fibration}
\label{sec:the_simple_fibration}
\input{simple}
% section the_simple_fibration (end)


\appendix

\input{appendix}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: