\chapter{Logical Foundations of Mathematics}
\label{chap:logical-foundations-of-mathematics}

In this chapter, we dive deeper into the logical foundations of Lean.

\section{Type Universes}
\label{sec:type-universes}

In type theory---and in particular in Lean---not only all terms have a type,
but also all types have a type themselves. We have already seen one occurrence
of this principle. The Curry--Howard correspondence tells us to view proofs as
terms and propositions as types. For example:
%
\[\hbox{\li{@and.intro : ∀a b, a → b → a ∧ b}}\]
%
Thus, a proposition such as \li{∀a b, a → b → a ∧ b} is a type, and this type
has in turn a type, namely \li{Prop}:
%
\[\hbox{\li{∀a b, a → b → a ∧ b : Prop}}\]
%
What is the type of \li{Prop} then? \li{Prop} has the same type as virtually
all other types we have constructed so far, namely, \li{Type}:
%
\[\begin{array}{l}
\mathbb{N}\mathtt{~{:}~Type} \\
\mathtt{Prop~{:}~Type}
\end{array}\]
%
What is the type of \li{Type}? It may seem like the simplest solution to assign
\li{Type : Type}, but this choice leads to Girard's paradox, the type theory
equivalent of Russel's paradox. To avoid inconsistencies, we need a fresh type
to contain \mbox{\li{Type},} which we call \li{Type 1}. \li{Type 1} again cannot be
assigned any of the other types introduced so far without causing
contradictions, leading to the introduction of \li{Type 2}, and so on:
%
\[\begin{array}{l}
\mathtt{Type~{:}~Type~1} \\
\mathtt{Type~1~{:}~Type~2} \\
\mathtt{Type~2~{:}~Type~3} \\
\quad\vdots
\end{array}\]
%
In fact, \li{Type} is an abbreviation for \li{Type 0}. If we want to
incorporate \li{Prop} in this hierarchy, we can also use the syntax
\li{Sort u}, where \li{Sort 0} is the same as \li{Prop} and \li{Sort (u + 1)} is
the same as \li{Type u}.

All of these types containing other types are called (\emph{type})
\emph{universes}, and the \li{u} in the expression \li{Sort u} is a
\li{universe level}. Although universe levels look like terms of type \li{ℕ},
they are in fact neither of type \li{ℕ} nor even terms.
% The only building blocks allowed to construct universe levels
% are universe variables \li{u}, zero
% \li{0}, successor \li{_ + 1},
% and the operators \li{max} and \li{imax}.

To formalize most of computer science and mathematics, \li{Type} (i.e.,
\li{Type 0}) suffices. Instead of using \li{Type} everywhere though, you can
make your theorems slightly more general without having to think about universe
levels by writing \mbox{\li{Type*},} which abbreviates \li{Type _}. It leaves it up to
Lean figure out the right universe level or to create a fresh universe variable.

% Lean's type hierarchy is \emph{noncumulative}: Each type lives only in one universe

% (This is different in Coq, where \li{p : Type u} implies \li{p : Type v} for all \li{v ≥ u})

% We can use \li{ulift : Type u → Type (max u v)} to transport types between type universes

% Constants can also be polymorphic in the type universe, and can be annotated with type universes—e.g., \li|eq.{u}|.

\section{The Peculiarities of Prop}
\label{sec:the-peculiarities-of-prop}

Although \li{Prop} seems to fit nicely into the hierarchy of type universes,
it is different from the other universes in many respects.

\subsection{Impredicativity}

When constructing a new type from other types (e.g., \li{α → β}
from \li{α : Type u} and \li{β : Type v}), the newly constructed type is
more complex than each of its components, and it is natural to put it into
the largest type universe involved (e.g., \li{α → β : Type (max u v)}).
This is exactly what Lean does. The following typing rule expresses this idea
generally for dependent types:
%
\begin{gather*}
\prftree[r]{\textsc{Pi}}
  {\text{\li{\Γ ⊢ α : Type u}}}
  {\text{\li{\Γ, (a : α) ⊢ β a : Type v}}}
  {\text{\li{\Γ ⊢ (Πa : α, β a) : Type (max u v)}}}
\end{gather*}
%
This behavior of the universes \li{Type v} is called \emph{predicativity}.

However, it is convenient to have \li{Prop} behave differently. We would like
\li{∀(a : Prop), a → a} to be of type \li{Prop}. Unfolding the syntactic sugar
\li{∀} and \li{→}, this expression is the same as \li{Π(a : Prop) (x : a), a}.
If we had \li{Type u} instead of \li{Prop}, the above typing rule would yield
%
\[\hbox{\li{(Π(a : Type u) (x : a), a) : Type (u + 1)}}\]
%
because \li{Type u : Type (u + 1)} and \li{max (u + 1) (max u u) = u + 1}.
Thus the universe level is increased by one when typing this expression.
To force expressions such as \li{∀(a : Prop), a → a}
(which equals \li{Π(a : Prop) (x : a), a})
to be of type \li{Prop} anyway, we have a special typing rule
for \li{Π} expressions involving \li{Prop}:
%
\begin{gather*}
    \prftree[r]{\textsc{Pi}}
      {\text{\li{\Γ ⊢ α : Sort u}}}
      {\text{\li{\Γ, (a : α) ⊢ β a : Prop}}}
      {\text{\li{\Γ ⊢ (Πa : α, β a) : Prop}}}
\end{gather*}
%
This is called \emph{predicativity} of \li{Prop}. The rule yields
%
\[\hbox{\li{(Π(a : Prop) (x : a), a) : Prop}}\]
%
as desired. The two typing rules for \li{Π} expressions above can be summarized
in one rule
\begin{gather*}
    \prftree[r]{\textsc{Pi}}
      {\text{\li{\Γ ⊢ α : Sort u}}}
      {\text{\li{\Γ, a : α ⊢ β a : Sort v}}}
      {\text{\li{\Γ ⊢ (Πa : α, β a) : Sort (imax u v)}}}
\end{gather*}
where
\begin{lstlisting}
imax u 0 = 0
imax u v = max u v   if v ≠ 0
\end{lstlisting}
%
In other systems, such as Agda, all type universes are predicative.

\subsection{Proof Irrelevance}

% Johannes: Impredicativity works because Lean has proof irrelevance ???
% What about Coq?

A second difference between \li{Prop} and \li{Type} is proof irrelevance.
It means that any two proofs of the same proposition are equal:
%
\lstinputlisting[linerange=proof_irrel-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
In Lean, this equality is even a definitional equality, allowing us to prove
that any two proofs of the same proposition are equal using the \li{refl}
tactic. When viewing a proposition as a type and a proof as an element of that
type, proof irrelevance means that a proposition is either an empty type or has
exactly one inhabitant. If it is empty, it is false. If it has exactly one
inhabitant, it is true. Proof irrelevance is very helpful when reasoning about
dependent types.

Other systems and logics make different choices in this matter. For example,
Agda and Coq are proof relevant by default, but are compatible with proof
irrelevance. Homotopy type theory and other \emph{constructive} or
\emph{intuitionistic} type theories build on data in equality proofs and
are therefore incompatible with proof irrelevance.

\subsection{Small Elimination}

A further difference between \li{Prop} and \li{Type} is that \li{Prop} does not
allow \emph{large elimination}, meaning that it
is impossible to extract data from a proof of a proposition. 
Consider the following inductive type:
%
\lstinputlisting[linerange=square_roots-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
The type \li{square_roots sq} contains all square roots of a given
integer \li{sq}. It contains no elements if \li{sq} is not square, one element if \li{sq = 0},
and two elements otherwise. For example:
%
\lstinputlisting[linerange=square_roots_examples-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
A large eliminator can be defined as follows:
%
\lstinputlisting[linerange=square_roots_large_elim-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
This eliminator's first explicit argument an element of \li{square_roots sq}.
The second one is a function that
converts a number and a proof that \li{sq} is the square of that number
into an element of an arbitrary type \li{α}.
Given those two things, it can produce the element of \li{α}
corresponding to the given element of \li{square_roots sq}.
For example, it can be used to extract the number that was used to construct
the given element of \li{square_roots}:
%
\lstinputlisting[linerange=square_roots_reduce-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
Therefore, the large eliminator can be used to prove that two elements of
\li{square_roots} are different if they were constructed using different roots:
%
\lstinputlisting[linerange=square_roots_neq-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
(This proof could be written more elegantly using the \li{cases} tactic.)

Moreover, the large eliminator
can be used to show that all numbers with a square root are nonnegative:
%
\lstinputlisting[linerange=square_roots_nonneg-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
(This proof could be written more elegantly using the \li{cases} tactic, too)

Now we make a second definition that strongly resembles \li{square_roots}. The
only difference is that we define it as an inductive predicate, i.e., we put
into the \li{Prop} universe instead of \li{Type u}.
%
\lstinputlisting[linerange=square_number-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
Again, we can show that \li{4} is square using either \li{2} or \li{-2}:
%
\lstinputlisting[linerange=square_number_examples-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
The following lemma is one that we can only prove for \li{square_number}, even
though we cannot prove the corresponding lemma for \li{square_roots}. We can
show that the two definitions above are equal, as a consequence of proof
irrelevance:
%
\lstinputlisting[linerange=square_number_eq-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
Proof irrelevance forces the type \li{square_number 4} to contain only one
element. Therefore, this element cannot contain the information as to whether
it was constructed using \li{2} or \li{-2}. This is why large elimination on
\li{square_number} would lead to an inconsistency and hence Lean will not allow
us to define a large eliminator:
%
\lstinputlisting[linerange=square_number_large_elim-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
But without being able to eliminate the \li{square_number} predicate at all, it
would be quite useless. As a compromise, Lean allows us to define a \emph{small
eliminator}:
%
\lstinputlisting[linerange=square_number_small_elim-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
It is called a small eliminator because it eliminates only into \li{Prop},
whereas a large eliminator can eliminate into an arbitrary large type universe
\li{Sort v}. This eliminator cannot be used to prove that \li{four_is_square}
and \li{four_is_square'} are different, but it can be used to prove that all
square numbers are nonnegative, just like we could with the large eliminator:
%
\lstinputlisting[linerange=square_number_nonneg-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%

% All inductive types living in \li{Type u} allow large elimination,
% while most of the inductive types living in \li{Prop}, i.e., inductive predicates,
% allow only small elimination.
% Only for inductive types fulfilling certain conditions,
% called \emph{syntactic subsingletons}, Lean
% makes an exception because under these conditions
% large elimination cannot be used to prove that there
% However, if \li{c} is a "syntactic subsingleton" (e.g., \li{false}, \li{∧}, \li{=}, \li{well_founded}), a large eliminator is generated

% > A "syntactic subsingleton" is an inductive definition with at most one constructor whose arguments are either \li{Prop} or appear as immediate arguments in the output type

% This exception is called \emph{subsingleton elimination}

\section{The Axiom of Choice}
\label{sec:the-axiom-of-choice}

To understand the axiom of choice, it will help to first take a look at the
following inductive predicate:
%
\begin{lstlisting}
inductive nonempty (α : Sort u) : Prop
| intro (val : α) : nonempty
\end{lstlisting}
%
The predicate states that the given type \li{α} has at least one element. To
prove \li{nonempty α}, we must provide an element of \li{α} to the \li{intro}
rule:
%
\lstinputlisting[linerange=nonempty_nat-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
Since \li{nonempty} lives in \li{Prop}, large elimination is not available, and
thus we cannot extract the element that was used from a proof of
\li{nonempty α}.

The axiom of choice allows us to obtain some element of type \li{α} if we can
show \li{nonempty α}:
%
\begin{lstlisting}
axiom classical.choice {α : Sort u} : nonempty α → α
\end{lstlisting}
%
We have no way of knowing whether this is the element that was used to prove
\li{nonempty α}. It will just give us an arbitrary element of \li{α}, thereby
avoiding inconsistencies.

The constant \li{classical.choice} is noncomputable. If we ask Lean for its
value using \li{#reduce} or \li{#eval}, it will refuse to compute it. This is
one of the reasons why some logicians prefer to work without this axiom. Unlike
proof irrelevance and the eliminators, this principle is not built into the
Lean kernel; it is only an axiom in Lean's core library, giving users the
freedom to work with or without it. Lean requires us to mark definitions as
\li{noncomputable} if they use \li{choice} to define constants outside of
\li{Prop}.

The following tools rely on \li{choice}:

\begin{itemize}
\item The function \li{classical.some} can help us find a witness of
\li{∃a : α, p a}, if we do not care which one.
%
\begin{lstlisting}
classical.some : (∃a : α, p a) → α
classical.some_spec (h : ∃a : α, p a) : p (some h)
\end{lstlisting}

\item We can also derive the traditional axiom of choice:
%
\begin{lstlisting}
classical.axiom_of_choice : ∀α β {r : α → β → Prop},
  (∀x : α, ∃y : β, r x y) → (∃f, ∀x, r x (f x))
\end{lstlisting}

\item The \li{choose} tactic provides an elegant way to use the
set theoretic version of the axiom of choice in proofs:
%
\lstinputlisting[linerange=choose-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}

\item Using \li{choice} and two other principles called propositional
extensionality and functional extensionality, the law of excluded middle can be
derived:
%
\begin{lstlisting}
classical.em : ∀p : Prop, p ∨ ¬ p
\end{lstlisting}
%
With the law of excluded middle, every proposition is decidable. This means
that we can construct proofs based on a case distinction on whether a certain
proposition is true. The \li{by_cases} tactic offers a convenient interface for
such proofs. To be able to use it with any proposition, add the line
%
\lstinputlisting[linerange=prop_decidable-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
at the top of your file.
Then you can use the \li{by_cases} tactic as follows:
%
\lstinputlisting[linerange=prop_decidable_ex-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
In this example, the line \li{by_cases h : p} introduces a case distinction
on whether \li{p} is true. It splits the goal into two subgoals, one with the
additional assumption \li{h : p}, the other with the additional assumption
\li{h : ¬ p}.
\end{itemize}

\section{Subtypes}
\label{sec:subtypes}

Subtyping is a mechanism to create new types from existing ones.
Given a predicate on the elements of the original type,
the new type contains only those elements of the original type
that fulfill this property.

To illustrate this, we will define a type of full binary trees, building on the
example from Section~\ref{sec:example-binary-trees}. In that section, we
defined an inductive type \li{btree}, representing binary trees. In
Section~\ref{sec:example-full-binary-trees}, we introduced a predicate
\li{is_full} that is true if each node of a tree has either zero or two child
nodes. Based on this type and this predicate, we can construct a subtype
\li{full_btree}, containing only full binary trees, as follows:
%
\lstinputlisting[linerange=full_btree-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
This is syntactic sugar for
%
\lstinputlisting[linerange=full_btree_sugarfree-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
where \li{subtype} is defined as an inductive predicate:
\begin{lstlisting}
inductive subtype {α : Type} (p : α → Prop) : Type
| mk : Πx : α, p x → subtype
\end{lstlisting}
Thus, every element of \li{full_btree} consists of a binary tree \li{t} and a proof that
\li{t} is full:
%
\lstinputlisting[linerange=some_full_btree-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
From a given element of \li{full_btree}, we can retrieve its two components via
\li{subtype.val} and \li{subtype.property}. For example:
%
\lstinputlisting[linerange=val_prop-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%

We can transfer functions from the base type \li{btree} to the subtype \li{full_btree}
if they preserve the property \li{is_full}.
As we have already shown in the lemma \li{is_full_mirror} in
Section \ref{sec:example-full-binary-trees},
\li{mirror} does preserve the property \li{is_full}.
We can use that lemma to define a function \li{full_btree.mirror}
operating on our new subtype as follows:
%
\lstinputlisting[linerange=full_btree_mirror-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
The input of the function is an element \li{t} of our subtype \li{full_btree}.
We decompose it into the binary tree \li{subtype.val t} and the proof of being full
\li{subtype.property t}. We use the \li{mirror} function to mirror the tree component
and the lemma \li{is_full_mirror} to transform the proof component into a proof
that the mirrored tree is full. Finally, we recompose the elements using
\li{subytpe.mk} into an element of our subtype.

For proofs about subtypes, the lemma \li{subtype.eq} is useful. It states that
two elements of a subtype are equal if their \li{subtype.val} components are
equal. Here is how it can be used to prove that the mirror image of a mirror
image of a \li{full_btree} is the \li{full_btree} itself:
%
\lstinputlisting[linerange=full_btree_mirror_mirror-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
The lemma \li{subtype.eq} allows us to transform the goal into
\li{mirror (mirror (subtype.val t)) = subtype.val t}, which matches the statement of the lemma
\li{mirror_mirror} we proved earlier. The two \li{unfold} calls help understand
the proof but are not necessary.

As a second example, consider the following definition of vectors from
\li{mathlib}:
%
\lstinputlisting[linerange=vec-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
Here, a vector is defined as a list of a given length. With lists, there is
only one type for a list of all lengths. For vectors, we have one dedicated type
for every length of a vector. The advantage of this is that some operations
such as addition or scalar product of vectors rely on the two involved vectors
having the same length.

Vectors can be built from lists using \li{subtype.mk} or the angle bracket
notation:
%
\lstinputlisting[linerange=some_vec-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
Basic operations on vectors can be defined by decomposing them with \li{subtype.val}
and \li{subtype.property}, manipulating the underlying lists, and then
recomposing them with \li{subtype.mk}.
For example, we can define the negation of an integer vector as follows:
%
\lstinputlisting[linerange=neg-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
We use \li{list.map} to negate every entry of the underlying list and
\li{list.length_map} to show that this operation does not change the
length of the list.
Using \li{subtype.eq}, we can prove the following lemma about this new operator:
%
\lstinputlisting[linerange=neg_neg-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
The application of  \li{subtype.eq} reduces the goal to showing the corresponding property
on the underlying lists. We can then use the lemmas \li{int.neg_comp_neg}
and \li{list.map_id},
which state \li{int.neg ∘ int.neg = id} and \li{∀xs : list α, map id xs = xs}, respectively.

\section{Quotient Types}
\label{sec:quotient-types}

Quotients are a powerful construction in mathematics used to define \li{ℤ},
\li{ℝ}, and many other sets. Lean supports \emph{quotient types}, an analogous mechanism on types. 
Just like subtypes, quotient types construct a new type
from an existing type. Unlike a subtype, a quotient type contains all of the
elements of the underlying type---but some elements that were different in the
underlying type are considered equal in the quotient type.

The prerequisites to construct a quotient type are a type \li{base} and an
equivalence relation
\li{e : base → base → Prop} specifying which elements of \li{base} will be considered
equal in the quotient. 
To construct the quotient type, we first need to declare \li{e} 
as an equivalence relation on \li{base}.
A type with an equivalence relation is called a \emph{setoid}.
In Lean, \li{setoid} is a type class, of which we can declare an instance as follows:
%
\lstinputlisting[linerange=setoid-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
As a side effect, this instance declaration allows us to use the notation 
\li{a ≈ b} for \li{e a b}. More importantly,
we can define the quotient type 
%
\lstinputlisting[linerange=my_quotient_type-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
Every element \li{a} in \li{base} belongs to
some element in \li{my_quotient}. We can find that element using
%
\begin{lstlisting}
quotient.mk : base → my_quotient
\end{lstlisting}
%
As an abbreviation for \li{quotient.mk a}, we can also write \li{⟦a⟧}.
The axiom \li{quotient.sound} guarantees that elements for which the relation
\li{e} holds are indeed equal in the quotient type:
%
\begin{lstlisting}
quotient.sound : ∀ {a b : base}, a ≈ b → ⟦a⟧ = ⟦b⟧
\end{lstlisting}
%
The lemma \li{quotient.exact} gives us the other direction:
%
\begin{lstlisting}
quotient.exact : ∀ {a b : base}, ⟦a⟧ = ⟦b⟧ → a ≈ b
\end{lstlisting}
%
Finally, we can \emph{lift} functions from \li{base → β} into \li{my_quotient → β}
using \li{quotient.lift}, which has the following computation rule. Given some
\li{f : base → β} such that \li{h : ∀a b, a ≈ b → f a = f b}, we have 
%
\[\hbox{\li{quotient.lift f h ⟦a⟧ = f a}}\]
%
for all \li{a : base}.
We can think of \li{quotient.lift} as an eliminator.

\subsection{Construction of the Integers}

As an example for a quotient type, we will
now construct the integers. A construction that turns out to be very convenient
is to construct a quotient over pairs of natural numbers (i.e., \li{ℕ × ℕ}).
The idea is that a pair \li{(m, n)} of natural numbers represents the integer
\li{m - n}. In this way, we can represent all nonnegative integers \li{m} by
\li{(m, 0)} and all negative integers \li{-n} by \li{(0, n)}. In addition, we
get many more representations of the same integers, e.g., \li{(2, 1)},
\li{(3, 2)}, and \li{(4, 3)} all represent the integer~\li{1}.

First, we need to register the equivalence
relation that we want to use. We want two pairs \li{(k, l)} and \li{(m, n)} to
be equal when \li{k - l} and \li{m - n} yield the same integer. However, the
condition \li{k - l = m - n} does not work because the negation on \li{ℕ} does
not behave like the negation on integers, e.g., \li{0 - 1 = 0}. Instead, we
use the condition \li{k + n = m + l}, which contains only addition.

We provide the definition of
our equivalence relation, followed by a proof that it is indeed a equivalence
relation (i.e., that it is reflexive, symmetric, and transitive):
%
\lstinputlisting[linerange=int_rel-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
We can now write \li{≈} for our equivalence relation:
%
\lstinputlisting[linerange=rel_iff-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
Using the name \li{myℤ.rel} of our \li{setoid} instance that we registered above,
we can then define the integers as
%
\lstinputlisting[linerange=int_def-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
We can define the integer zero as
%
\lstinputlisting[linerange=int_zero-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
In fact, any term of the form \li{⟦(n, n)⟧} represents the same integer:
%
\lstinputlisting[linerange=int_more_zeros-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
Next, we define addition on our newly constructed integers.
To define functions on a quotient type, one can define the
function on the original type first, and then \emph{lift} the
definition to the quotient type. To do that, we must prove
that the definition of the function \li{f} does not depend on
the chosen representative of an equivalence class, i.e.,
\li{a ≈ b → f a = f b}.
The functions
\li{quotient.lift} (for unary functions)
and \li{quotient.lift₂} (for binary functions)
can be used to lift functions in this way.

Addition can be defined as simply adding the pairs of natural numbers
componentwise. We then need provide a proof that this can be lifted to
a function on the quotient by showing that \li{a₁ ≈ b₁}
and \li{a₂ ≈ b₂} imply
\li{⟦(a₁.1 + a₂.1, a₁.2 + a₂.2)⟧ = ⟦(b₁.1 + b₂.1, b₁.2 + b₂.2)⟧}:
%
\lstinputlisting[linerange=int_add-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
This yields a function \li{add} with the intended behavior:
%
\lstinputlisting[linerange=int_add_mk-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
We can use this to prove other lemmas about \li{add}, such as
%
\lstinputlisting[linerange=int_add_zero-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}

\section{Summary of New Syntax}

\small

\subsection{Tactics}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
  \li|by_cases| & makes a case distinction on whether a given statement is true \\
  \li|choose| & applies the axiom of choice to a hypothesis of the form
  \li{\∀}\dots\,\li{\∃}\dots \\
\end{tabularx}

\subsection{Constants}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
  \li|classical.choice| & function that returns an arbitrary element of a nonempty type\\
  \li|classical.some| & function that returns a witness given a proof of an existential \\
  \li|Prop| & abbreviation for \li{Sort 0} \\
  \li|quot| & function that creates a quotient type given an arbitrary
  relation \\
  \li|quotient| & function that creates a quotient type of a given setoid
  instance \\
  \li|setoid| & type class for a type with an equivalence relation on it \\
  \li|Sort u| & type universe at level \li{u} \\
  \li|Type u| & abbreviation for \li{Sort (u + 1)} \\
\end{tabularx}

\subsection{Notation}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
  \li|\{x : α // p x\}| &  subtype of all \li{x} in \li{\α} fulfilling the predicate \li{p}\\
  \li|\≈| & equivalence relation on a setoid \\
\end{tabularx}
