移民后不久，小柯尔斯坦的父母为了让他改掉吮手指的坏习惯，骗他说吮手指的小孩子在英国会被警察叔叔剪掉大拇指。没过多久，他们就发现小彼得竟然站在一大堆警察面前吮手指，还一边 (用德语) 问警察：“你们的剪刀呢？” 由此可见，柯尔斯坦在很小的时候就是一个实验主义者了。

# Week 1

# HoTT in type theory context

• ITT (Intensional type theory) is a intuitionistic type theory that serves as the core theory for other type theories. Other type theories are merely extensions of ITT .

• ETT (Extensional type theory) extends ITT with ER (equality of reflection) and UIP (uniqueness of identity proofs):

  $$ETT=ITT+RT+UIPS$$

  Since types are perceived as sets in ETT , ETT gives rise to a intuitionistic theory of sets.

• HoTT extends ITT with HIT (higher inductive types) and UA (univalence axiom):

  $$HoTT=ITT+HIT+UA$$

  Since types are perceived as abstract spaces in HoTT , HoTT gives rise to a intuitionistic theory of $weak\;\infty-groupoids$.

# Intuitionistic propositional logic

Intuitionistic logic means it is a proof-relevant logic.

• As advanced by Per Matin-Lof, a modern presentation of IPL (intuitionistic propositional logic) distinguishes the notions of judgment and proposition.

  A judgment is something that may be known, whereas a proposition is something that sensibly may be the subject of a judgment.

  In IPL , the two most basic judgements are A prop and A true:

  • A prop A is a well-formed proposition
  • A true Proposition A is intuitionistically true, i.e., has a proof.

• The inference rules for the prop judgment are called formation rules.

  The inference rules for the true judgment are divided into classes: introduction rules and elimination rules.

# Negative fragment of IPL

# Conjunction

$$\begin{aligned} \frac{A\;prop\quad B\;prop}{A\wedge B\;prop}\quad & (\wedge F)\\ \frac{A\;true\quad B\;true}{A\wedge B\;true}\quad & (\wedge I)\\ \frac{A\wedge B\;true}{A\;true}\quad &(\wedge E_1)\\ \frac{A\wedge B\;true}{B\;true}\quad &(\wedge E_2) \end{aligned}$$

# Truth

Another familiar and simple proposition is truth, which is denoted by $\top$.

$$\begin{aligned} \frac{}{\top\;prop}\quad & (\top F)\\ \frac{}{\top\;true}\quad & (\top I) \end{aligned}$$

# Entailment

The last form of proposition in the negative fragment of IPL is implication.
However, to define implication, a different form of judgment is required: entailment, which is written as:

$$\begin{aligned} \underbrace{A_1\;true, \dots, A_n\;true}_{n \geq 0}\vdash A\;true \end{aligned}$$

we can understand the left part as the “context”, denoted by $\Gamma$, or the assumptions for $A\;true$. So we can rewrite the conjunction as:

$$\begin{aligned} \frac{\Gamma\vdash A\;true\quad \Gamma\vdash B\;true}{\Gamma\vdash A\wedge B\;true}\quad(\wedge I) \end{aligned}$$

Reflexivity:

$$\frac{}{A\;true\vdash A\;true}\quad (R)$$

Transitivity:

$$\frac{A\;true\quad A\;true\vdash C\;true}{C\;true}\quad (T)$$

---

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
substructural logics.

Weakening:

$$\frac{A\;true}{B\;true\vdash A\;true}\quad (W)$$

Contraction:

$$\frac{A\;true,A\;true\vdash C\;true}{A\;true\vdash C\;true}\quad (C)$$

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.

Permutation:

$$\frac{\Gamma\vdash C\;true}{\pi(\Gamma)\vdash C\;true}\quad (P)$$

where $\pi(\Gamma)$ is a permutation of $\Gamma$.

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.

# Implication

$$\begin{aligned} \frac{A\;prop\quad B\;prop}{A\supset B\;prop}\quad (\supset F)\\ \end{aligned}$$

The introduction rule for implication is:

$$\begin{aligned} \frac{A\;true\vdash B\;true}{A\supset B\;true}\quad (\supset I) \end{aligned}$$

We use implication to internalize the entailment as a proposition: $B\;true\vdash A\;true$ is not a proposition while $B\supset A$ is a proposition.

We may write the elimination rule as $\frac{A\supset B\;true}{A\;true\vdash B\;true}$. However, we can consider “$A\;true\vdash B\;true$” as some stuff like function. We would prefer the uncurried form of elimination rule, which is:

$$\begin{aligned} \frac{A\supset B\;true\quad A\;true}{B\;true}\quad (\supset E) \end{aligned}$$

it’s somehow “(A, B) -> C” instread of “A -> (B -> C)”.

# Positive fragment of IPL

# Disjunction

$$\begin{aligned} \frac{A\;prop\quad B\;prop}{A\vee B\;prop}\quad (\vee F)\\ \end{aligned}$$

The introduction rule for disjunction is:

$$\begin{aligned} \frac{A\;true}{A\vee B\;true}\quad (\vee I_1)\\ \frac{B\;true}{A\vee B\;true}\quad (\vee I_2) \end{aligned}$$

The elimination rule for disjunction is:

$$\begin{aligned} \frac{A\vee B\;true\quad A\;true\vdash C\;true\quad B\;true\vdash C\;true}{C\;true}\quad (\vee E) \end{aligned}$$

# Falsehood

The unit of disjunction is falsehood, the proposition that is trivially never true, which we write as $\perp$. Its formation rule is immdeidate evidence that $\perp$ is a well-formed proposition:

$$\begin{aligned} \frac{}{\perp\;prop}\quad (\perp F) \end{aligned}$$

Because $\perp$ is never true, it has no introduction rule. However, it does have an elimination rule, which captures “ex falso quolibet”:

$$\begin{aligned} \frac{\perp\;true}{C\;true}\quad (\perp E) \end{aligned}$$

# Order-theoretic formulation of IPL

# Conjunction as meet

The elimination rules for conjunction (along with reflexivity of entailment) ensure
that $A\wedge B\;true\vdash A\;true$ and $A\wedge B\;true\vdash B\;true$.
To ensure completeness of the order-theoretic formulation, we include the rules:

$$\begin{aligned} \frac{}{A\wedge B\leq A}\quad\frac{}{A\wedge B\leq B} \end{aligned}$$

which say that $A\wedge B$ is a lower bound of A and B.

The introduction rule for conjunction ensures that $C\;true\vdash A\wedge B\;true$ if both
$C\;true\vdash A\;true$ and $C\;true\vdash B\;true$. Order-theoretically, this is expressed as the rule:

$$\frac{C\leq A\quad C\leq B}{C\leq A\wedge B}$$

which says that $A\wedge B$ is larger than or equal to any lower bound of A and B.
Taken together these rules show that $A\wedge B$ is the greatest lower bound, or meet, of A and B.

# Truth as greatest element

The introduction rule for truth ensures that $C\;true\vdash \top\;true$. Order-theoretically, we have

$$\frac{}{C\leq \top}$$

which says that $\top$ is the greatest, or final element.

# Disjunction as join

The introduction rules for disjunction ensure that $A\vee B\;true\vdash A\;true$ and $A\vee B\;true\vdash B\;true$, we include the rules:

$$\frac{}{A\leq A\vee B}\quad\frac{}{B\leq A\vee B}$$

which say that $A\vee B$ is an upper bound of A and B.

The elimination rule for disjunction (along with reflexivity of entailment) ensures that
$A\vee B\;true\vdash C\;true$ if both $A\;true\vdash C\;true$ and $B\;true\vdash C\;true$.
Order-theorectically, we have the rule:

$$\frac{A\leq C\quad B\leq C}{A\vee B\leq C}$$

which says that $A\vee B$ is as small as any upper bound of A and B.
Taken together these rules show that $A\vee B$ is the least upper bound, or join, of A and B.

# Falsehood as least element

The elimination rule for falsehood (along with reflexivity of entailment) ensures that
$\perp\;true\vdash C\;true$. The order-theoretic counterpart is:

$$\frac{}{\perp\leq C}$$

which says that $\perp$ is the least, or initial element.

# Implication as exponential

The elimination rule for implication (along with reflexivity of entailment) ensures that
$A\;true,A\supset B\;true\vdash B$. For the order-theoretic formulation to be complete, we include the rule:

$$\frac{}{A\wedge(A\supset B)\leq B}$$

The introduction rule for implication ensures that $C\;true\vdash A\supset B\;true$ if
$A\;true,C\;true\vdash B\;true$. We have:

$$\frac{A\wedge C\leq B}{C\leq A\supset B}$$

Taken together, $A\supset B$ is the exact upper bound of the set $\{X\;|\;A\wedge X\leq B\}$.

What’s more, we can consider $A\supset B$ as the exponential: $B^A$.
Why? We use a more familiar denotation “$A\rightarrow B$” for implication, you may realize that the set of functions from set A to set B is also denoted as $B^A$.
The process of currying and uncurrying is just the arithmetic law:

$$\begin{aligned} & A\rightarrow (B\rightarrow C)\cong (C^B)^A=C^{B*A}\cong (A\wedge B) \rightarrow C\\ \end{aligned}$$

# Week 2

# Lindenbaum algebra

Recall that IPL has the structure of a preorder, where we declare $A\leq B$ if and only if $A\;true\vdash B\;true$.
Let $T$ be some theory in IPL and define a relation $\simeq$ on the propositions in $T$ by:

$$A\simeq B\quad if\;and\;only\;if\quad A\leq B\;and\;B\leq A$$

Obviously, $\simeq$ is an equivalence relation.

# Decidability and stability

Decidability is what separates constructive logic from classic logic: in classic logic, every proposition is decidable while in constructive logic, it’s not.

• $\perp,\top$ are decidable.
• We would expect $m=_\mathbb{N}n$ is decidable, where $=_\mathbb{N}$ denotes the quality of natural numbers.
• we would not expect $m=_\mathbb{R}n$ is decidable, where $=_\mathbb{R}$ denotes the quality of real numbers, because they are infinite.

Again, in classic logic, every proposition is stable, while in constructive logic let’s consider the following lemma:

Proof:
$\neg A=A\supset\perp$.

We must show $\neg(A\vee\neg A)\supset\perp\;true$.

• We first prove $\neg(A\vee\neg A)\;true\vdash A\supset\perp\;true$:

$$\begin{aligned} \cfrac{\cfrac{A\;true}{A\vee\neg A\;true}(\vee I_1)\quad \neg(A\vee\neg A)\;true}{\perp}(\supset E) \end{aligned}$$

• So in fact,$\neg(A\vee\neg A)\;true\vdash\neg A\;true$.
  Then we have

$$\cfrac{\cfrac{\neg A\;true}{A\vee\neg A\;true}(\vee I_2)\quad \neg(A\vee\neg A)\;true}{\perp}(\supset E)$$

So

$$\cfrac{\neg(A\vee\neg A)\;true\vdash\perp}{\neg(A\vee\neg A)\supset\perp\;true}(\supset I)$$

The lemma says the exclude middle proposition $A\vee\neg A$ is not stable since $\neg\neg(A\vee\neg A)$ can be proved but $A\vee\neg A$ cannot.

# Disjunctive property

A theory T has the DP (disjunctive property) if $T\vdash A\vee B$ implies $T\vdash A$ or $T\vdash B$.

Naive attempt at a proof: The idea is to perform induction on all
possible derivations $\nabla$ of $\emptyset\vdash A\vee B\;true$.
Since $\emptyset\vdash A\vee B\;true$ can only be obtained by $\vee I_1,\vee I_2$ and $\supset E,\wedge E,\vee E,\perp E$.

If:

$$\cfrac{\cfrac{\nabla}{A\;true}}{\emptyset\vdash A\vee B\;true}(\vee I_1)$$

Here we already obtained a proof for $A\;true$, $\vee I_2$ is just similar.

If:

$$\cfrac{\cfrac{\nabla_1}{\emptyset\vdash C\supset A\vee B\;true}\quad\cfrac{\nabla_2}{\emptyset \vdash C\;true}}{\emptyset\vdash A\vee B\;true}(\supset E)$$

then we can find that since $\emptyset\vdash C\supset A\vee B\;true$, there must be a proof for $C\;true\vdash A\vee B\;true(\supset I)$.
The we can use $\nabla_2$ to substitute all the occurence in $\nabla_1$ for $C\;true$. Then we get a smaller derivation for $\emptyset\vdash A\vee B\;true$. Thus we can repeat the process and in finite repeatation we can fall back on $\vee I_1$ or other deduction rules.

# Admissible properties

Proof:
Firstly we can prove that Reflexivity, Contraction and Exchange are admissible. Take Reflexivity as an example:

$$\cfrac{\Gamma\vdash A\;true}{\Gamma\vdash A\;true}(R)$$

it is admissible in that it can be substituted by:

$$\cfrac{\cfrac{\Gamma\vdash A\;true}{\Gamma\vdash A\wedge A\;true}(\wedge I)}{\Gamma\vdash A\;true}(\wedge E)$$

And for contraction, for any derivation $\cfrac{\cfrac{\nabla}{A\;true,A\;true\vdash C\;true}}{A\;true\vdash C\;true}$ we can substitute any $A\;true,A\;true$ in $\nabla$ by $A\;true$.
So the rule does not change anything.

For weakening rule, we need to use the induction:

Suppose that $\cfrac{\Gamma\vdash B_1\;true}{\Gamma,A\;true\vdash B_1\;true}$ and $\cfrac{\Gamma\vdash B_2\;true}{\Gamma,A\;true\vdash B_2\;true}$ are admissible, then there will be derivation without weakening for them:

$$\cfrac{\Gamma\vdash B_1\;true}{\cfrac{\nabla_1(no\;weakening)}{\Gamma,A\;true\vdash B_1\;true}}\quad \cfrac{\Gamma\vdash B_2\;true}{\cfrac{\nabla_2(no\;weakening)}{\Gamma,A\;true\vdash B_2\;true}}$$

then we can prove that $\cfrac{\Gamma\vdash B_1\wedge B_2\;true}{\Gamma,A\;true\vdash B_1\wedge B_2\;true}$ is also admissible:

$$\cfrac{\cfrac{\cfrac{\cfrac{\Gamma\vdash B_1\wedge B_2\;true}{\Gamma\vdash B_1\;true}(\wedge E_1)}{\nabla_1}}{\Gamma,A\;true\vdash B_1\;true}\quad\cfrac{\cfrac{\cfrac{\Gamma\vdash B_1\wedge B_2\;true}{\Gamma\vdash B_2\;true}(\wedge E_2)}{\nabla_2}}{\Gamma,A\;true\vdash B_2\;true}}{\Gamma,A\;true\vdash B_1\wedge B_2\;true}$$

Then by induction we can shrink the derivation, until the proposition don’t have “$\wedge,\vee,\neg$”. The last proposition is proved by some rules other than weakening, so the weakening is admissible.

Other rules are proved in the same way. In a word, structural properties (Reflexivity, Contraction, Exchange, Weakening, Transitivity) are admissible, while negative and positive fragments (conjunction,disjunction)
are not.

# Proof terms

# Proof terms as variables

We use the notation $M:A$ to denote that $M$ is a proof of proposition $A$.
To track the proofs, we will write:

$$x_1:A_1,...,x_n:A_n\vdash M:A$$

where each $x_i:A_i$ is a proof term.
We can think $x_1,...,x_n$ as the hypothesis for the proof,
but what we really want is for them to behave like varaibles, the proof
$M$ will use the variables to prove.

# Structural Properties of Entailment with Proof Terms

• Reflexivity/Variable rule:

$$\cfrac{}{\Gamma,x:A,\Gamma'\vdash x:A}(R/V)$$

• Transitivity/Substitution

$$\cfrac{\Gamma,x:A,\Gamma'\vdash N:B\quad\Gamma\vdash M:A}{\Gamma,\Gamma'\vdash [M/x]N:B}(T/S)$$

which means, if the previous proof can prove the proposition $A$, then $x:A$ is no longer needed. We can substitute $x$ with $M$ in the proof $N$ of $B$.

• Weakening:

$$\cfrac{\Gamma\vdash M:A}{\Gamma,\Gamma'\vdash M:A}(W)$$

• Contraction:
  If we have two different proofs for the same proposition $x:A,y:A$,then we can pick one of them $z=x$ or $z=y$ and substitute the other one with $z$:

$$\cfrac{\Gamma,x:A,y:A,\Gamma'\vdash N:B}{\Gamma,z:A,\Gamma'\vdash [z/x\;or\;z/y]N:B}(C)$$

• Exchange:

$$\cfrac{\Gamma,x:A,y:B,\Gamma'\vdash N:C}{\Gamma,y:B,x:A,\Gamma'\vdash N:C}(X)$$

# Negative fraggment of IPL with proof terms

• Truth: truth is trivially always true, so it doesn’t need any proof:

$$\cfrac{}{\Gamma\vdash\langle\;\rangle:\top}(\top I)$$

• Conjunction Introduction:We combine the proof $M,N$ as $\langle M,N\rangle$:

$$\cfrac{\Gamma\vdash M:A\quad \Gamma\vdash N:B}{\Gamma\vdash \langle M,N\rangle:A\wedge B}(\wedge I)$$

• Conjunction Elimination:

$$\cfrac{\Gamma\vdash M:A\wedge B}{\Gamma\vdash fst(M):A}(\wedge E_1) \quad \cfrac{\Gamma\vdash M:A\wedge B}{\Gamma\vdash snd(M):B}(\wedge E_2)$$

• Implication Introduction: we may view the proof $x$ as a variable:

$$\cfrac{\Gamma,x:A\vdash M:B}{\Gamma\vdash \lambda x.M:A\supset B}$$

• Implication Elimination:

$$\cfrac{\Gamma\vdash M:A\supset B\quad\Gamma\vdash N:A}{\Gamma \vdash M(N):B}(\supset E)$$

# Identity of proofs

# Definitional equality

We need the definitional equality to define the equality of two proofs:$M:A,M':A$ are the same. We denote it as $M\equiv M':A$ and want it to be the least congruence containing(closed under) the $\beta$ rules.

A congruence is an equivalence relation that respects our operations, for the equivalence relation that respects our operations, it basically means that if $M\equiv M':A$, then that their images under any operator should be equivalent. In
other words, we should be able to replace $M$ with $M'$ everywhere. For example, it shoule be true that:

$$\cfrac{\Gamma\vdash M\equiv M':A\wedge B}{\Gamma\vdash fst(M)\equiv fst(M'):A}$$

There might be many congruences that contains the $\beta$ rules. Given two congruences $\equiv$ and $\equiv'$, we say
$\equiv$ is finer that $\equiv'$ if $M\equiv' M':A$ implies $M\equiv M':A$.

# Gentzen’s Inversion Principle

Gentzen’s Inversion Principle captures the intuition that “the elimination rules should cancel the introduction rules modulo definitional equility”.

The following are the $\beta$ rules for the negative fragment of IPL :

Conjunction:

$$\cfrac{\Gamma\vdash M:A\quad\Gamma\vdash N:B}{\Gamma\vdash fst(\lang M,N\rang)\equiv M:A\wedge B}(\beta\wedge_1)\\ \cfrac{\Gamma\vdash M:A\quad\Gamma\vdash N:B}{\Gamma\vdash snd(\lang M,N\rang)\equiv N:A\wedge B}(\beta\wedge_2)$$

Implication:

$$\cfrac{\Gamma,x:A\vdash M:B\quad\Gamma\vdash N:A}{\Gamma\vdash (\lambda x.M)(N)\equiv[N/x]M:B}(\beta\supset)$$

# Gentzen’s Unicity Principle

Gentzen’s Unicity Principle captures the intuition that “there should be one way to prove something under definitional equivalence”.

Truth:

$$\cfrac{\Gamma\vdash M:\top}{\Gamma\vdash M\equiv \lang\;\rang:\top}(\eta\top)$$

Conjunction:

$$\cfrac{\Gamma\vdash M:A\wedge B}{\Gamma\vdash M\equiv\lang fst(M),snd(M)\rang:A\wedge B}(\eta\wedge)$$

Implication:

$$\cfrac{\Gamma\vdash M:A\supset B}{\Gamma\vdash M\equiv\lambda x.M(x):A\supset B}(\eta\supset)$$

# Proposition as types

There is a correspondence between propositions and types:

Propositions	Types
$\top$	1
$A\wedge B$	$A\times B$
$A\supset B$	$A\rightarrow B$ or $B^A$
$\perp$	0
$A\vee B$	$A+B$

Later we will see the objects of the types introduced in the right column.

# Categorical Theoretic Approach

In a Heyting Algebra, we have a preorder $A\leq B$ when
$A$ implies $B$.
However, we now wish to keep track of proofs, so if $M$
is a proof from $A$ to $B$, we want to think it as a map
$M:A\rightarrow B$.

Identity map:

$$id:A\rightarrow A$$

Composition:
We should be able to compose maps:

$$\cfrac{f:A\rightarrow B\quad g:B\rightarrow C}{g\circ f:A\rightarrow C}$$

Coherence Conditions:

$$id_B\circ f=f:A\rightarrow B\\ f\circ id_A=f:A\rightarrow B\\ h\circ(g\circ f)=(h\circ g)\circ f:A\rightarrow D$$

Now we can think about objects in the category that corresponds to propositions given in the correspondence.

Terminal Object:
1 is the terminal object, also called the final object,
which corresponds to $\top$. For any object $A$ there is a unique map $A\rightarrow 1$. This corresponds to $\top$ being the greatest object in a Heyting Algebra, meaning that for all $A$, $A\leq 1$.

Existence:

$$\langle\;\rangle:A\rightarrow 1$$

Uniqueness:

$$\cfrac{M:A\rightarrow 1}{M=\langle\;\rangle:A\rightarrow 1}(\eta\top)$$

Product:
For any objects $A$ and $B$ there is an object $C=A\times B$ that is the product of $A$ and $B$, which corresponds to the join $A\wedge B$. The product $A\times B$ has the following universal property:

where the diagram commutes.

First, the existence condition means that there are maps:

$$fst:A\times B\rightarrow A\\ snd:A\times B\rightarrow B$$

The universal property says that for every object $D$ such that $M:D\rightarrow A$ and $N:D\rightarrow B$, there exists a unique map $\langle M,N\rangle:D\rightarrow A\times B$ such that:

$$\cfrac{M:D\rightarrow A\quad N:D\rightarrow B}{\langle M,N\rangle:D\rightarrow A\times B}$$

and the diagram commutes meaning

$$fst\circ\langle M,N\rangle=M:D\rightarrow A\\ snd\circ\langle M,N\rangle=N:D\rightarrow B$$

Furthermore, the map $\langle M,N\rangle:D\rightarrow A\times B$ is unique in the sense that

$$\cfrac{P:D\rightarrow A\times B\quad fst\circ P=M:D\rightarrow A\quad snd\circ P:D\rightarrow B}{P=\langle M,N\rangle:D\rightarrow A\times B}$$

so in other words, $\langle fst\circ P,snd\circ P\rangle=P$.

Another way to say above is:

$$\langle fst,snd\rangle=id\\ \langle M,N\rangle\circ P=\langle M\circ P,N\circ P\rangle$$

Exponential:
Given objects $A$ and $B$, an exponential $B^A$ (which corresponds to $A\supset B$) is an object with the following universal property:

such that the diagram commutes.
This means that there exists a map $ap:B^A\times A\rightarrow B$ (application map) that corresponds to implication elimination.

The universal property is that for all objects $C$ that have a map $h:C\times A\rightarrow B$, there exists a unique map $\lambda(h):C\rightarrow B^A$ such that:

$$ap\circ(\lambda(h)\times id_A)=h:C\times A\rightarrow B$$

This means that the diagram commutes. Another way to express the induced map is $\lambda(h)\times id_A=\langle \lambda(h)\circ fst,snd\rangle$.\
The map $\lambda(h):C\rightarrow B^A$ is unique, meaning that

$$\cfrac{ap\circ(g\times id_A)=h:C\times A\rightarrow B}{g=\lambda(h):C\rightarrow B^A}(\eta)$$

# Week3

# The $\beta$ and $\eta$ rules

# Gentzen’s Inversion Principles ($\beta$ rules)

Recall the $\beta$ rules:

$$\begin{aligned} & \wedge_1:fst\langle M,N\rangle\equiv M\\ & \wedge_2:snd\langle M,N\rangle\equiv N\\ & \supset_1:(\lambda x.M)(N)\equiv [N/x]M\\ & \vee_1:case(inl(M);x.P,y.Q)\equiv[M/x]P\\ & \vee_2:case(inr(M);x.P,y.Q)\equiv[M/y]Q \end{aligned}$$

where $case(x;y,z)$ means if x then y else z. $inl(M)$ means that in
the proof $M$, we use the left proof $x:P$ and $\vee_1$ to prove $P\vee Q$.

# Gentzen’s Unicity Principles ($\eta$ rules)

Recall the $\eta$ rules we have given so far:

Truth:

$$\cfrac{\Gamma\vdash M:\top}{\Gamma\vdash M\equiv\langle\;\rangle}(\eta\top)$$

Conjunction:

$$\cfrac{\Gamma\vdash M:A\wedge B}{\Gamma\vdash M\equiv\lang fst(M),snd(M)\rang:A\wedge B}(\eta\wedge)$$

Implication:

$$\cfrac{\Gamma\vdash M:A\supset B}{\Gamma\vdash M\equiv\lambda x.M(x):A\supset B}(\eta\supset)$$

Conjunction:

$$\cfrac{\Gamma\vdash M:A\wedge B\quad \Gamma\vdash fst(M)\equiv P:A\quad \Gamma\vdash snd(M)\equiv Q:B}{\Gamma\vdash M\equiv\lang P,Q\rang:A\wedge B}(\eta\wedge)$$

which says that given any object $C$ with maps $P:C\rightarrow A$ and $Q:C\rightarrow B$, there exists a unique map $\langle P,Q\rangle:C\rightarrow A\times B$ such that the $\beta$ rules make each cell commute, meaning $P\equiv fst(\langle P,Q\rangle,Q\equiv snd(\langle P,Q\rangle)$.