gistfile1.txt

\documentclass[11pt]{article}

%%%%       %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% LAGDA %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%       %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\usepackage{amssymb, amsmath, tikz-qtree}

%include agda.fmt
%include polycode.fmt

\usepackage{color}
\newcommand{\redFG}[1]{\textcolor[rgb]{0.6,0,0}{#1}}
\newcommand{\greenFG}[1]{\textcolor[rgb]{0,0.4,0}{#1}}
\newcommand{\blueFG}[1]{\textcolor[rgb]{0,0,0.8}{#1}}
\newcommand{\purpleFG}[1]{\textcolor[rgb]{0.4,0,0.4}{#1}}
\newcommand{\orangeFG}[1]{\textcolor[rgb]{0.8,0.4,0}{#1}}
\newcommand{\blackFG}[1]{\textcolor[rgb]{0,0,0}{#1}}

\newcommand{\D}[1]{\blueFG{\textsf{#1}}}    % data types
\newcommand{\C}[1]{\redFG{\textsf{#1}}}     % constructors
\newcommand{\F}[1]{\greenFG{\textsf{#1}}}   % functions
\newcommand{\V}[1]{\purpleFG{\textit{#1}}}  % variables
\newcommand{\FD}[1]{\orangeFG{\textsf{#1}}} % accessors

%subst conid a = "\V{" a "}"
%subst varid a = "\V{" a "}"
%format constructor = "\Keyword{constructor}"
%format λ = "\D{$\lambda$}"
%format Set = "\D{Set}"

%%%%   section 0

%format Tree = "\D{Tree}"
%format lf = "\C{lf}"
%format _br_ = "\_\!\cdot\!\_"

\begin{document}

\begin{center}\textit{Catamorphisms, Universal Properties, and Preorder Reasoning}\end{center}

The Curry-Howard correspondence provides a very useful connection
between the world of constructive logic on the one hand, and the world
of computation on the other. Essentially, the correspondence says that
logical propositions correspond to programming types, and proofs of
propositions correspond to inhabitants of the types. The most common
version of this is the Brouwer-Heyting-Kolmogorov (BHK)
interpretation. In this interpretation, we have some simple
correspondences:

\begin{center}
	\begin{tabular}{|c|c|c|}
		\hline
		Proposition & Type & Term\\
		\hline\hline
		$True$ & $\top$ & $tt$\\
		\hline
		$False$ & $\bot$ & none\\
		\hline
		$P \wedge Q$ & $P \times Q$ & $(p,q)$\\
		\hline
		$P \vee Q$ & $P + Q$ & $inl\ p$ or $inr\ q$\\
		\hline
		$P \Rightarrow Q$ & $P \to Q$ & $\lambda x. y$\\
		\hline
	\end{tabular}
\end{center}

Different logics usually employ subtle variations of this depending on
how much the logic is supposed to do, or what sorts of things are
supposed to be proven. For instance, the programming language Haskell
uses a type system that corresponds roughly to sentential logic with
propositional operators and universal quantification over
propositions. But then, Haskell's goal is to be a practical
programming language. A language like Agda, on the other hand, is
intended to be used both for programming but \textit{also} for
constructive proofs of propositions in higher order logic, and as such
its type system is dependently typed, derived from Luo's UTT (itself a
derivative of Martin-L\"{o}f's intuitionistic type theory). Agda
provides an appropriate balance between the proof side of things, and
the computation side of things, that makes it rather useful for doing
syntactic theory in formal, computationally assisted ways.\\

In the following sections, I will use Agda in overviewing some
interesting, and hopefully theoretically useful, ideas. To start,
let's define a data type to represent just the shape of
single-dominance binary trees.

\begin{code}
  data Tree : Set where
    lf : Tree
    _br_ : Tree -> Tree -> Tree
\end{code}

This type lets us represent the shape of trees quite easily. For
example, the tree in (\ref{aTree}) is represented using this type as
(\ref{aTreeRep}).

\begin{enumerate}
  \item\label{aTree} \Tree [ [ {\ } {\ } ] {\ } ]
\end{enumerate}

\textbf{Catamorphisms}\\

A catamorphism is 

\end{document}