notes_week1.tex

% arara: pdflatex
% arara: bibtex
% arara: pdflatex
% arara: pdflatex
\documentclass[12pt]{article}

\usepackage{lmodern}
\usepackage{microtype}

% Package for customizing page layout
\usepackage[letterpaper]{geometry}
% \usepackage{fullpage}

\input{macros}

\usepackage{proof-dashed}
\usepackage{tikz-cd}

\metadata{DeYoung and Balzer}{2013/09/09 and 2013/09/11}

% \usepackage{parskip}
% \setlength{\parskip}{0.1cm}
% \setlength{\parindent}{0mm}

\begin{document}

\title{15-819 Homotopy Type Theory\\ Lecture Notes}
\author{Henry DeYoung and Stephanie Balzer}
\date{September 9 and 11, 2013}

\maketitle

% [COMMENT_SB:]

% > Should we have a title for inference-rule based formulation of IPL?

% > Is it Brouwer's program, principle, or dictum?

\section{Contents}\label{sec:contents}

These notes summarize the lectures on \ac{HoTT} given by Professor Robert Harper on September 9
and 11, 2013, at CMU.  They start by providing a introduction to \ac{HoTT}, capturing its main
ideas and its connection to other related type theories.  Then they present \ac{IPL}, giving
both an proof-theoretic formulation as well an order-theoretic formulation.

% [COMMENT_SB:] How does IPL relate to HoTT?

\section{Introduction to \acl{HoTT}}\label{sec:intro}

\Acf{HoTT} is the subject of a very active research community that gathered at the Institute
for Advanced Study (IAS) in 2012 to participate in the Univalent Foundations Program.  The
results of the program have been recently published in the \ac{HoTT} Book~\cite{HoTTBook2013}.

\subsection{\Acs{HoTT} in a nutshell}\label{subsec:hott_in_nutshell}

\Ac{HoTT} is based on Per Martin-L\"{o}f's \acl{TT}, which provides a foundation for
\emph{intuitionistic mathematics} and which is an extension of \emph{Brouwer's program}.
Brouwer viewed mathematical reasoning as a human activity and mathematics as a language for
communicating mathematical concepts.  As a result, Brouwer perceived the ability of executing a
step-by-step procedure or algorithm for performing a \emph{construction} as a fundamental human
faculty.

Adopting Brouwer's constructive viewpoint, intuitionistic theories view proofs as the
fundamental forms of construction.  The notion of \emph{proof relevance} is thus a
characteristic feature of an intuitionistic (or constructive\footnote{In this course,
  intuitionism and constructivism are used interchangeably.}) approach.  In the context of
\ac{HoTT}, proof relevance means that proofs become mathematical objects~\cite{Harper2013}.  To
fully understand this standpoint, it is necessary to draw a distinction between the notion of a
\emph{proof} and the one of a \emph{formal proof}~\cite{Harper2013,Harper2012}.  A formal proof
is a proof given in a fixed formal system, such as the axiomatic theory of sets, and arises
from the application of the inductively defined rules in that system.  Whereas every formal
proof is also a proof (assuming soundness of the system) the converse is not true.  This fact
immediately follows from G\"{o}del's Incompleteness Theorem, which precisely states that there
exist true propositions (with a proof), but for which there cannot be given a formal proof,
using the rules of the formal system.  Unlike conventional formally defined systems, \ac{HoTT}
does not surmise that all possible proofs can be fully circumscribed by its rules, but accepts
proofs that cannot be formalized in \ac{HoTT}.  These are exactly the proofs that are
considered to be \emph{relevant} and, being treated as mathematical objects, they can be
formulated internally as objects of the type theory.

Being based on \acl{TT}, \acs{HoTT} facilitates some form of axiomatic freedom.  This means in
particular that there exist fewer assumptions that apply globally.  For instance, a typical
such assumption that is missing in a intuitionistic interpretation is the \acl{LEM}.  As put
forth by Brouwer, an assumption like the \acl{LEM} does not need to be ruled out entirely, but
can be introduced locally, in a proof, if needed.  Whether a particular local assumption is
needed or not is mainly determined by the actual proof (i.e., construction).  A sparing use of
global assumptions results in proofs that are based on less assumptions and thus in stronger
results overall.

Another distinguishing characteristics of \acs{HoTT} is that it adopts a \emph{synthetic},
rather than an \emph{analytic} reasoning approach.  The differentiation goes back to Lawvere
and is best explained by an example.  Euclidean geometry, for instance, represents a synthetic
approach to geometry as it treats geometric figures, like triangles, lines, and circles, as
``things'' in themselves rather than sets of points.  In an analytical approach based on the
Cartesian coordinate system, on the other hand, geometric figures are treated as sets of points
in the plane and thus are based on the real numbers.  Whereas traditional formulations of
homotopy theory are analytic, \acs{HoTT} is synthetic.  The differentiation between a synthetic
and an analytic reasoning approach is mainly relevant with regard to the approach's amenability
to mechanized reasoning.  It turns out that synthetic approaches are easier to mechanize than
analytical approaches.  This holds true in particular for \acs{HoTT}: since proofs of equality
in \acs{HoTT} correspond to paths in a space, they are cleaner, shorter, and completely
mechanizable.

\subsection{\Acs{HoTT} in type theory context}\label{subsec:type_theory_context}

\Ac{HoTT} unites homotopy theory with type theory, by embodying Brouwer's intuitionism and
drawing from Gentzen's proof theory (see Section~\ref{sec:ipl}).  It is based on the
observation that \emph{types} classify the admissible forms of constructions and thus are
programmatically sufficient to encompass all known mathematical constructions.  This section
briefly sketches how \ac{HoTT} relates to other existing type theories.

\subsubsection{\Acl{ITT}}

\Acf{ITT} is a \acl{TT} that serves as the core theory for other type theories.  Other type theories
are merely extensions of \acs{ITT}.

\subsubsection{\Acl{ETT}}

\Acf{ETT} extends \acs{ITT} with equality of reflection (ER) and uniqueness of identity proofs (UIP):

\begin{equation*}
ETT = ITT + ER + UIP
\end{equation*}

\noindent Since types are perceived as sets in \acs{ETT}, \acs{ETT} gives rise to a
intuitionistic theory of sets.

\subsubsection{\Acl{HoTT}}

\Acs{HoTT} extends \acs{ITT} with higher inductive types (HIT) and the univalence axiom (UA):


\begin{equation*}
HoTT = ITT + HIT + UA
\end{equation*}

\noindent Since types are perceived as abstract spaces in \acs{HoTT}, \acs{HoTT} gives rise to
a intuitionistic theory of \emph{weak infinity groupoids}.

\section{\Acl{IPL}}\label{sec:ipl}

What is meant by \emph{intuitionistic} logic?  It is a \emph{proof-relevant}
logic.  One might say its slogan is ``logic as if people matter'', alluding to
Brouwer's principle that mathematics is a social process in which proofs are
crucial for communication.  Whenever a claim of truth of a proposition is made,
it must be accompanied by a proof.

As advanced by Per Martin-L\"{o}f, a modern presentation of \acf{IPL} distinguishes the notions of \vocab{judgment} and \vocab{proposition}.
A judgment is something that may be known, whereas a proposition is something that sensibly may be the subject of a judgment.
For instance, the statement ``Every natural number larger than $1$ is either prime or can be uniquely factored into a product of primes\@.'' is a proposition because it sensibly may be subject to judgment.
That the statement is in fact true is a judgment.
Only with a proof, however, is it evident that the judgment indeed holds.

Thus, in \ac{IPL}, the two most basic judgments are $A \prop$ and $A \true$:
\begin{alignat*}{2}
  A \prop &&\quad& \text{$A$ is a well-formed proposition} \\
  A \true &&& \text{\begin{tabular}[t]{@{}l@{}}
                Proposition $A$ is intuitionistically true, \\
                i.e., has a proof.
              \end{tabular}}
\end{alignat*}
The inference rules for the $\prop$ judgment are called formation rules.
The inference rules for the $\true$ judgment are divided into classes:  \vocab{introduction rules} and \vocab{elimination rules}.

Following Martin-L\"{o}f, the meaning of a proposition $A$ is given by the introduction rules for the judgment $A \true$.
The elimination rules are dual and  describe what may be deduced from a proof of $A \true$.

The principle of \vocab{internal coherence}, also known as Gentzen's principle of inversion, is that the introduction and elimination rules for a proposition $A$ fit together properly.  The elimination rules should be strong enough to deduce all information that was used to introduce $A$ (\vocab{local completeness}), but not so strong as to deduce information that might not have been used to introduce $A$ (\vocab{local soundness}).  In a later lecture, we will discuss internal coherence more precisely, but we can already give an informal treatment.

\subsection{Negative fragment of \ac{IPL}}\label{sec:ipl-negative}

\subsubsection{Conjunction}\label{sec:conjunction}

One familiar group of propositions are the conjunctions.
If $A$ and $B$ are well-formed propositions, then so is their conjunction, which we write as $A \conj B$.
This is the content of the formation rule for conjunction: it serves as evidence of the judgment $A \conj B \prop$, provided that there is evidence of the judgments $A \prop$ and $B \prop$.
\begin{equation*}
  \infer[{\conj}F]{A \conj B \prop}{
    A \prop & B \prop}
\end{equation*}

We have yet to give meaning to conjunction, however; to do so, we must say how to introduce the judgment that $A \conj B$ is \emph{true}.
As the following rule shows, a verification of $A \conj B$ consists of a proof of $A \true$ paired with a proof of $B \true$.
\begin{equation*}
  \infer[{\conj}I]{A \conj B \true}{
    A \true & B \true}
\end{equation*}

What may we deduce from the knowledge that $A \conj B$ is true?
Because every proof of $A \conj B \true$ ultimately introduces that judgment from a pair of proofs of $A \true$ and $B \true$, we are justified in deducing $A \true$ and $B \true$ from any proof of $A \conj B \true$.
This leads to the elimination rules for conjunction.
\begin{mathpar}
  \infer[{\conj}E_1]{A \true}{
    A \conj B \true}
  \and
  \infer[{\conj}E_2]{B \true}{
    A \conj B \true}
\end{mathpar}

\paragraph{Internal coherence.}\label{sec:conj-coherence}
As previously mentioned, the principle of internal coherence says that the introduction and elimination rules fit together properly: the elimination rules are strong enough, but not too strong.

If we mistakenly omitted the ${\conj}E_2$ elimination rule, then there would be no way to
extract the proof of $B \true$ that was used in introducing $A \conj B \true$---the elimination
rules would be too weak.

On the other hand, if we mistakenly wrote the ${\conj}I$ introduction rule as
\begin{equation*}
  \infer{A \conj B \true}{
    A \true} \,,
\end{equation*}
then there would be no proof of $B \true$ present to justify deducing $B \true$ with the ${\conj}E_2$ rule---the elimination rules would be too strong.

\subsubsection{Truth}\label{sec:truth}

Another familiar and simple proposition is \vocab{truth}, which we write as $\truth$.
Its formation rule serves as immediate evidence of the judgment $\truth \prop$, that $\truth$ is indeed a well-formed proposition.
\begin{equation*}
  \infer[{\truth}F]{\truth \prop}{
    }
\end{equation*}

Once again, to give meaning to truth we must say how to introduce the judgment that $\truth$ is true.
$\truth$ is a trivially true proposition, and so its introduction rule makes the judgment $\truth \true$ immediately evident.
\begin{equation*}
  \infer[{\truth}I]{\truth \true}{
    }
\end{equation*}

We should also consider an elimination rule: from a proof of $\truth \true$, what can we deduce?
Since $\truth$ is trivially true, any such elimination rule would not increase our knowledge---we put in no information when we introduced $\truth \true$, so, by the principle of conservation of proof, we should get no information out.
For this reason, there is no elimination rule for $\truth$, and we can see that its absence is coherent with the introduction rule.

\paragraph{The nullary conjunction.}\label{sec:nullary-conjunction}
An observation about $\truth$ that often proves useful is that $\truth$ behaves as a nullary conjunction---a conjunction over the empty set of conjuncts, rather than over a set of two conjuncts.

This observation is reflected in the inference rules.
Just as the introduction rule for binary conjunction has two premises (one for each of the two conjuncts), the introduction rule for truth has no premises (one for each of the no conjuncts):
\begin{mathpar}
  \infer[{\conj}I]{A \conj B \true}{
    A \true & B \true}
  \and
  \infer[{\truth}I]{\truth \true}{
    }
\end{mathpar}
Likewise, just as there are two elimination rules for binary conjunction, there are no elimination rules for truth:
\begin{mathpar}
  \infer[{\conj}E_1]{A \true}{
    A \conj B \true}
  \and
  \infer[{\conj}E_2]{B \true}{
    A \conj B \true}
  \and\and
  \text{(no ${\truth}E$ rule)}
\end{mathpar}

\subsubsection{Entailment}\label{sec:entailment}

The last form of proposition in the negative fragment of \ac{IPL} is implication.
However, to define implication, a different form of judgment is required: entailment (also known as logical consequence or a hypothetical judgment).
Entailment is written as
\begin{equation*}
  \underbrace{A_1 \true, \dotsc, A_n \true}_{n \geq 0} \entails A \true \,,
\end{equation*}
and expresses the idea that the judgment $A \true$ follows from $A_1 \true, \dotsc, A_n \true$.
You can think of $A_1 \true, \dotsc, A_n \true$ as being assumptions from which the conclusion $A \true$ may be deduced.
The metavariable $\ctx$ is typically used to stand for such a context of assumptions.

We should note that, thus far, the inference rules have been presented in a \vocab{local form} in which the context of assumptions was left implicit.
It would also be possible to make this context explicit.
For example, the introduction rule for conjunction in the two different forms is:
\begin{mathpar}
  \infer[{\conj}I]{A \conj B \true}{
    A \true & B \true}
  \and
  \infer[{\conj}I]{\ctx \entails A \conj B \true}{
    \ctx \entails A \true &
    \ctx \entails B \true}
\end{mathpar}
In the remainder of these notes, we will write inference rules in local form whenever possible.

As an entailment, the judgment form satisfies several \emph{structural properties}: reflexivity, transitivity, weakening, contraction, and permutation.

\paragraph{Reflexivity.}\label{sec:reflexivity}
If the entailment judgment is to express logical consequence, that is, that a conclusion follows from some assumptions, then you must accept a principle of reflexivity,
\begin{equation*}
  \infer[\text{\textsf{R}}]{A \true \entails A \true}{
    } \,,
\end{equation*}
that an assumption is enough to conclude the same judgment.
If you tried to deny this principle, the meaning of an assumption would be unclear.

\paragraph{Transitivity.}\label{sec:transitivity}
Dual to reflexivity is a transitivity principle that states that a proof of a conclusion satisfies an assumption of the same judgment.
\begin{equation*}
  \infer[\text{\textsf{T}}]{C \true}{
    A \true &
    A \true \entails C \true}
\end{equation*}
Transitivity is a lemma rule.
If you prove a lemma ($A \true$), then you are justified in using it to prove a theorem that explicitly depends ($A \true \entails C \true$); taken together, they are \emph{viewed} as a direct proof of the theorem ($C \true$).

Transitivity can also be thought of as proof inlining.
Rather than pairing the lemma with the theorem that depends upon it, we could inline the lemma's proof at every point at which the theorem refers to the lemma.  The result is a truly direct proof of the theorem.

% Transitivity should be an \vocab{admissible rule}, meaning that it need not be included as an expicit rule since it can be proved as a metatheorem about the remaining rules.
% For transitivity, this corresponds to the computational notion of inlining.
% Rather than having the notion of ``lemma paired with theorem'' that arises from transitivity as an explicit rule, we can instead inline the lemma's proof

\paragraph{Weakening.}\label{sec:weakening}
Reflexivity and transitivity are undeniable properties of entailment because they give meaning to assumptions---assumptions are strong enough to prove conclusions (reflexivity), but are only as strong as the proofs they stand for (transitivity).
But there are also structural properties that can be denied: weakening, contraction, and
permutation.  Logics that deny any of these properties are called \emph{substructural logics}.

The principle of weakening says that we can add assumptions to a proof without invalidating that proof:
\begin{equation*}
  \infer[\text{\textsf{W}}]{B \true \entails A \true}{
    A \true}
\end{equation*}
Of course, the new proof is of a weaker statement, but it is nevertheless a valid proof.

Denying weakening leads, in part, to relevance logic.
It is called relevance logic because the proofs may not contain the unnecessary, irrelevant assumptions that weakening allows.
In this course, we will always have the principle of weakening, however.

\paragraph{Contraction.}\label{sec:contraction}
The principle of contraction says that we are unconcerned about the number of copies of an assumption $A \true$; one copy is as good as two:
\begin{equation*}
  \infer[\text{\textsf{C}}]{A \true \entails C \true}{
    A \true, A \true \entails C \true}
\end{equation*}

Denying contraction (along with weakening) leads to linear logic, in which we wish to reason about the number of copies of an assumption.
This is a powerful way to express consumable resources.
In this course, we will always have the principle of contraction, however.

\paragraph{Permutation.}\label{sec:permutation}
The principle of permutation, or exchange, says that the order of assumptions does not matter; we can apply any permutation $\pi$ to the assumptions and still have a valid proof:
\begin{equation*}
  \infer[\text{\textsf{P}}]{\pi(\ctx) \entails C \true}{
    \ctx \entails C \true}
\end{equation*}
(Note that it is difficult to state the permutation principle in local rule form.)

Denying permutation (along with weakening and contraction) leads to ordered, or noncommutative, logic.
It is a powerful way to express ordered structures, like lists or even formal grammars.
In this course, we will always have the principle of permutation, however.

\subsubsection{Implication}\label{sec:implication}

With the entailment judgment in hand, we can give rules for implication.

Like conjunction, if $A$ and $B$ are well-formed propositions, then so is their implication, which we write as $A \imp B$.
\begin{equation*}
  \infer[{\imp}F]{A \imp B \prop}{
    A \prop & B \prop}
\end{equation*}

Once again, to give meaning to implication, we must say how to introduce the judgment $A \imp B \true$.
To prove $A \imp B \true$, we assume $A \true$ and prove $B \true$.
\begin{equation*}
  \infer[{\imp}I]{A \imp B \true}{
    A \true \entails B \true}
\end{equation*}
In this way, implication internalizes the entailment judgment as a proposition, while we nonetheless maintain the distinction between propositions and judgments.
(As an aside for those familiar with category theory, the relationship between entailment and implication is analogous to the relationship between a mapping and a collection of mappings internalized as an object in some categories.)

This introduction rule for implication is the key distinction between Gentzen-style natural deduction calculus and a Hilbert-style axiomatic calculus.
In a Hilbert presentation of \ac{IPL}, there is no separate notion of entailment, making it difficult to reason hypothetically.
Instead, one must contort proofs to make use of several seemingly unmotivated axioms about implication.

Thankfully, we will work with natural deduction and be able to reason hypothetically using the introduction rule.
But what does the elimination rule for $A \imp B$ look like?
Because every proof of $A \imp B \true$ ultimately introduces that judgment from a proof of the entailment $A \true \entails B \true$, we might like to write the elimination rule as
\begin{equation*}
  \infer{A \true \entails B \true}{
    A \imp B \true} \,.
\end{equation*}
This is a valid principle of reasoning, but it turns out to be useful to instead adopt an uncurried form as the actual elimination rule:
\begin{equation*}
  \infer[{\imp}E]{B \true}{
    A \imp B \true & A \true} \,.
\end{equation*}
This rule is sometimes referred to as \latin{modus ponens}.

\paragraph{Internal coherence.}\label{sec:imp-coherence}
These introduction and elimination rules are coherent.
The elimination rule is strong enough to recover the entailment that any proof of $A \imp B \true$ ultimately uses in introduction, as the following derivation shows.
\begin{equation*}
  \infer[{\imp}E]{A \true \entails B \true}{
    \infer[\text{\textsf{W}}]{A \true \entails A \imp B \true}{
      A \imp B \true} &
    \infer[\text{\textsf{R}}]{A \true \entails A \true}{
      }}
\end{equation*}
On the other hand, the elimination rule is not too strong because it is just an uncurrying of the inverted introduction rule.

\subsection{Positive fragment of \ac{IPL}}\label{sec:positive}

\subsubsection{Disjunction}\label{sec:disjunction}

As for conjunction and implication, the disjunction, $A \disj B$, of $A$ and $B$ is a well-formed proposition if both $A$ and $B$ are themselves well-formed propositions.
\begin{equation*}
  \infer[{\disj}F]{A \disj B \prop}{
    A \prop & B \prop}
\end{equation*}

A disjunction $A \disj B$ may be introduced in either of two ways: $A \disj B$ is true if $A$ is true or if $B$ is true.
\begin{mathpar}
  \infer[{\disj}I_1]{A \disj B \true}{
    A \true}
  \and
  \infer[{\disj}I_2]{A \disj B \true}{
    B \true}
\end{mathpar}
To devise the elimination rule, consider what may we deduce from the knowledge that $A \disj B$ is true.
For $A \disj B$ to be true, it must have been ultimately introduced using one of the two introduction rules.
Therefore, either $A$ or $B$ is true (or possibly both).
The elimination rule allows us to reason by these two cases: If $C \true$ follows from $A \true$ and also follows from $B \true$, then $C$ is true in either case.
\begin{equation*}
  \infer[{\disj}E]{C \true}{
    A \disj B \true &
    A \true \entails C \true & B \true \entails C \true}
\end{equation*}

\subsubsection{Falsehood}\label{sec:falsehood}

The unit of disjunction is falsehood, the proposition that is trivially never true, which we write as $\falsehood$.  Its formation rule is immediate evidence that $\falsehood$ is a well-formed proposition.
\begin{equation*}
  \infer[{\falsehood}F]{\falsehood \prop}{
    }
\end{equation*}

Because $\falsehood$ should never be true, it has no introduction rule.
The elimination rule captures \latin{ex falso quodlibet}: from a proof of $\falsehood \true$, we may deduce that \emph{any} proposition $C$ is true because there is ultimately no way to introduce $\falsehood \true$.
\begin{equation*}
  \infer[{\falsehood}E]{C \true}{
    \falsehood \true}
\end{equation*}

Once again, the rules cohere.
The elimination rule is very strong, but remains justified due to the absence of any introduction rule for falsehood.

\paragraph{The nullary disjunction.}\label{sec:nullary-disjunction}
We previously noted that $\truth$ behaves as a nullary conjunction.
In the same way, $\falsehood$ behaves as a nullary disjunction.
For a binary disjunction, there are two introduction rules, ${\disj}I_1$ and ${\disj}I_2$, one for each of the two disjuncts; for falsehood, there are no introduction rules:
\begin{mathpar}
  \infer[{\disj}I_1]{A \disj B \true}{
    A \true}
  \and
  \infer[{\disj}I_2]{A \disj B \true}{
    B \true}
  \and
  \text{(no ${\falsehood}I$ rule)}
\end{mathpar}
Likewise, for a binary disjunction, there is one elimination rule with a premise for the disjunction and one premise for each of the disjuncts; for falsehood, there is one elimination rule with just a premise for falsehood:
\begin{mathpar}
  \infer[{\disj}E]{C \true}{
    A \disj B \true &
    A \true \entails C \true & B \true \entails C \true}
  \and
  \infer[{\falsehood}E]{C \true}{
    \falsehood \true}
\end{mathpar}

\section{Order-theoretic formulation of \acs{IPL}}\label{sec:ipl_order}

It is also possible to give an order-theoretic formulation of \ac{IPL} because entailment is a preorder (reflexive and transitive).
We want $A \leq B$ to hold exactly when $A \true \entails B \true$.
We can therefore devise the order-theoretic formulation with these soundness and completeness goals in mind.

\subsection{Conjunction as meet}\label{sec:conjunction-as-meet}

The elimination rules for conjunction (along with reflexivity of entailment) ensure that $A \conj B \true \entails A \true$ and $A \conj B \true \entails B \true$.
To ensure completeness of the order-theoretic formulation, we include the rules
\begin{mathpar}
  \infer{A \conj B \leq A}{
    }
  \and
  \infer{A \conj B \leq B}{
    } \,,
\end{mathpar}
which say that $A \conj B$ is a lower bound of $A$ and $B$.

The introduction rule for conjunction ensures that $C \true \entails A \conj B \true$ if both $C \true \entails A \true$ and $C \true \entails B \true$.
Order-theoretically, this is expressed as the rule
\begin{equation*}
  \infer{C \leq A \conj B}{
    C \leq A & C \leq B} \,,
\end{equation*}
which says that $A \conj B$ is as large as any lower bound of $A$ and $B$.
Taken together these rules show that $A \conj B$ is the greatest lower bound, or meet, of $A$ and $B$.

Graphically, these order-theoretic rules can be represented with a commuting \vocab{product diagram}, where arrows point from smaller to larger elements:
\begin{equation*}
  \begin{tikzcd}
    {} &[-4ex] C \ar[bend right]{ddl}\ar[bend left]{ddr}\dar[dashed] &[-4ex] {} \\
    {} & A \conj B \dlar\drar & {} \\
    A & {} & B
  \end{tikzcd}
\end{equation*}

\subsection{Truth as greatest element}\label{sec:truth-as-greatest}

The introduction rule for $\truth$ ensures that $C \true \entails \truth \true$.
Order-theoretically, we have 
\begin{equation*}
  \infer{C \leq \truth}{
    } \,,
\end{equation*}
which says that $\truth$ is the greatest, or final, element.

In the proof-theoretic formulation of \ac{IPL}, we saw that truth $\truth$ is the nullary conjunction.
We should expect this analogy to hold in the order-theoretic formulation of \ac{IPL} as well, and it does---the greatest element is indeed the greatest lower bound of the empty set.

\subsection{Disjunction as join}\label{sec:disjunction-as-join}

The introduction rules for disjunction (along with reflexivity of entailment) ensure that $A \true \entails A \disj B \true$ and $B \true \entails A \disj B \true$.
To ensure completeness of the order-theoretic formulation, we include the rules
\begin{mathpar}
  \infer{A \leq A \disj B}{
    }
  \and
  \infer{B \leq A \disj B}{
    } \,,
\end{mathpar}
which say that $A \disj B$ is an upper bound of $A$ and $B$.

The elimination rule for disjunction (along with reflexivity of entailment) ensures that $A \disj B \true \entails C \true$ if both $A \true \entails C \true$ and $B \true \entails C \true$.
Order-theoretically, we have the corresponding rule
\begin{equation*}
  \infer{A \disj B \leq C}{
    A \leq C & B \leq C} \,,
\end{equation*}
which says that $A \disj B$ is as small as any upper bound of $A$ and $B$.
Taken together these rules show that $A \disj B$ is the least upper bound, or join, of $A$ and $B$.

Graphically, this is captured by a commuting \vocab{coproduct diagram}:
\begin{equation*}
  \begin{tikzcd}
    A \drar\ar[bend right]{ddr} &[-4ex] {} &[-4ex] B \dlar\ar[bend left]{ddl}\\
    {} & A \disj B \dar[dashed] & {} \\
    {} & C & {}
  \end{tikzcd}
\end{equation*}

\subsection{Falsehood as least element}\label{sec:falsehood-as-least}

The elimination rule for falsehood (along with reflexivity of entailment) ensures that $\falsehood \true \entails C \true$.
The order-theoretic counterpart is the rule
\begin{equation*}
  \infer{\falsehood \leq C}{
    } \,,
\end{equation*}
which says that $\falsehood$ is the least, or initial, element.

Once again, because we saw that falsehood is the nullary disjunction in the proof-theoretic formulation, we should expect this analogy to carry over to the order-theoretic formulation.
Indeed, the least element is the least upper bound of the empty set.

\subsection{Order-theoretic \ac{IPL} as lattice}\label{subsec:lattice}

As seen thus far, the order-theoretic formulation of \ac{IPL} gives rise to a \vocab{lattice} as it establishes a
preorder with finite meets and joins.  The definition of a lattice assumed in this course may
deviate from the one typically found in the literature, which usually considers a lattice to be
a partial order with finite meets and joins.  In this course, we deliberately ignore the
property of antisymmetry.  If we were to impose the property of antisymmetry on the order
defined by entailment, then we would need to introduce equivalence classes of propositions,
which requires associativity.  As we will see later in this course, the axiom of univalence
provides an elegant way of dealing with equivalence of propositions.

\subsection{Implication as exponential}\label{sec:impl-as-expon}

The elimination rule for implication (along with reflexivity of entailment) ensures that $A \true, A \imp B \true \entails B \true$.
For the order-theoretic formulation to be complete, we include the rule 
\begin{equation*}
  \infer{A \conj (A \imp B) \leq B}{
    }
\end{equation*}
% which say that $A \conj B$ is a lower bound of $A$ and $B$.

The introduction rule for implication ensures that $C \true \entails A \imp B \true$ if $A \true, C \true \entails B \true$.
Once again, so that the order-theoretic formulation is complete, we have
\begin{equation*}
  \infer{C \leq A \imp B}{
    A \conj C \leq B} \,,
\end{equation*}
Taken together, these rules show that $A \imp B$ is the exponential of $A$ and $B$.

% The \vocab{exponential diagram} is:
% \begin{equation*}
%   \begin{tikzcd}
%     C \dar[dashed] \\
%     A \imp B
%   \end{tikzcd}
%   \begin{tikzcd}
%     A \conj (A \imp B) \\
%   \end{tikzcd}
% \end{equation*}

As we have seen previously, the order-theoretic formulation of \ac{IPL} gives
rise to a lattice.  Now we have just seen that it also supports exponentials.
As a result, the order-theoretic formulation of \ac{IPL} gives rise to a
\vocab{Heyting algebra}.  A Heyting algebra is a lattice with exponentials.  As
we will see later in this course, the notion of a Heyting algebra is fundamental
in proving completeness of \ac{IPL}.  The proof also relies on the notion of a
\vocab{complement} in a lattice.  The complement $\overline{A}$ of $A$ in a
lattice is such that
\begin{enumerate}
\item $\top\leq \overline{A}\vee A$;
\item $\overline{A}\wedge A \leq\bot$.
\end{enumerate}
It follows that a complement, if present, is a suitable notion of negation, but
negation, defined via the exponential, is not necessarily a complement.


\nocite{Pfenning2009a, Pfenning2009b}
\bibliographystyle{plain}
\bibliography{hott_references}

\end{document}