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

# 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+UIPSETT=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+UAHoTT=ITT+HIT+UA

    Since types are perceived as abstract spaces in HoTT , HoTT gives rise to a intuitionistic theory of weak  groupoidsweak\;\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

A  propB  propAB  prop(F)A  trueB  trueAB  true(I)AB  trueA  true(E1)AB  trueB  true(E2)\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.

  prop(F)  true(I)\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:

A1  true,,An  truen0A  true\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  trueA\;true. So we can rewrite the conjunction as:

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

Reflexivity:

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

Transitivity:

A  trueA  trueC  trueC  true(T)\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:

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

Contraction:

A  true,A  trueC  trueA  trueC  true(C)\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:

ΓC  trueπ(Γ)C  true(P)\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

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

The introduction rule for implication is:

A  trueB  trueAB  true(I)\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  trueA  trueB\;true\vdash A\;true is not a proposition while BAB\supset A is a proposition.

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

AB  trueA  trueB  true(E)\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

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

The introduction rule for disjunction is:

A  trueAB  true(I1)B  trueAB  true(I2)\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:

AB  trueA  trueC  trueB  trueC  trueC  true(E)\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:

  prop(F)\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”:

  trueC  true(E)\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 AB  trueA  trueA\wedge B\;true\vdash A\;true and AB  trueB  trueA\wedge B\;true\vdash B\;true.
To ensure completeness of the order-theoretic formulation, we include the rules:

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

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

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

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

which says that ABA\wedge B is larger than or equal to any lower bound of A and B.
Taken together these rules show that ABA\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  trueC\;true\vdash \top\;true. Order-theoretically, we have

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

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

# Disjunction as join

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

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

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

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

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

which says that ABA\vee B is as small as any upper bound of A and B.
Taken together these rules show that ABA\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
  trueC  true\perp\;true\vdash C\;true. The order-theoretic counterpart is:

C\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,AB  trueBA\;true,A\supset B\;true\vdash B. For the order-theoretic formulation to be complete, we include the rule:

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

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

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

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

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

A(BC)(CB)A=CBA(AB)C\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 ABA\leq B if and only if A  trueB  trueA\;true\vdash B\;true.
Let TT be some theory in IPL and define a relation \simeq on the propositions in TT by:

ABif  and  only  ifAB  and  BAA\simeq B\quad if\;and\;only\;if\quad A\leq B\;and\;B\leq A

Obviously, \simeq is an equivalence relation.

Definition. The Lindenbaum algebra of TT is defined to be the collection of \simeq-equivalence classes of propositions in TT. Write A=[A]A^*=[A]_\simeq. The ordering on the Lindenbaum algebra is inherited from \leq.

# Decidability and stability

Definition. A prop is decidable if and only if A¬A  trueA\vee\neg A\;true.

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=Nnm=_\mathbb{N}n is decidable, where =N=_\mathbb{N} denotes the quality of natural numbers.
  • we would not expect m=Rnm=_\mathbb{R}n is decidable, where =R=_\mathbb{R} denotes the quality of real numbers, because they are infinite.

Definition. A prop is stable if and only if (¬¬A)A  true(\neg\neg A)\supset A\;true.

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

Lemma. ¬¬(A¬A)  true\neg\neg(A\vee\neg A)\;true.

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

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

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

A  trueA¬A  true(I1)¬(A¬A)  true(E)\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,¬(A¬A)  true¬A  true\neg(A\vee\neg A)\;true\vdash\neg A\;true.
    Then we have

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

So

¬(A¬A)  true¬(A¬A)  true(I)\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¬AA\vee\neg A is not stable since ¬¬(A¬A)\neg\neg(A\vee\neg A) can be proved but A¬AA\vee\neg A cannot.

# Disjunctive property

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

Theorem. In IPL , if AB  true\emptyset\vdash A\vee B\;true then A  true\emptyset\vdash A\;true or B  true\emptyset\vdash B\;true.

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

If:

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

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

If:

1CAB  true2C  trueAB  true(E)\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 CAB  true\emptyset\vdash C\supset A\vee B\;true, there must be a proof for C  trueAB  true(I)C\;true\vdash A\vee B\;true(\supset I).
The we can use 2\nabla_2 to substitute all the occurence in 1\nabla_1 for C  trueC\;true. Then we get a smaller derivation for AB  true\emptyset\vdash A\vee B\;true. Thus we can repeat the process and in finite repeatation we can fall back on I1\vee I_1 or other deduction rules.

# Admissible properties

Definition. A deduction rule is admissible in IPL if nothing changes when it is added to the existing rules of IPL .

Theorem. The structural properties of IPL\vdash_{IPL} are admissible.

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

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

it is admissible in that it can be substituted by:

ΓA  trueΓAA  true(I)ΓA  true(E)\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 A  true,A  trueC  trueA  trueC  true\cfrac{\cfrac{\nabla}{A\;true,A\;true\vdash C\;true}}{A\;true\vdash C\;true} we can substitute any A  true,A  trueA\;true,A\;true in \nabla by A  trueA\;true.
So the rule does not change anything.

For weakening rule, we need to use the induction:

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

ΓB1  true1(no  weakening)Γ,A  trueB1  trueΓB2  true2(no  weakening)Γ,A  trueB2  true\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 ΓB1B2  trueΓ,A  trueB1B2  true\cfrac{\Gamma\vdash B_1\wedge B_2\;true}{\Gamma,A\;true\vdash B_1\wedge B_2\;true} is also admissible:

ΓB1B2  trueΓB1  true(E1)1Γ,A  trueB1  trueΓB1B2  trueΓB2  true(E2)2Γ,A  trueB2  trueΓ,A  trueB1B2  true\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:AM:A to denote that MM is a proof of proposition AA.
To track the proofs, we will write:

x1:A1,...,xn:AnM:Ax_1:A_1,...,x_n:A_n\vdash M:A

where each xi:Aix_i:A_i is a proof term.
We can think x1,...,xnx_1,...,x_n as the hypothesis for the proof,
but what we really want is for them to behave like varaibles, the proof
MM will use the variables to prove.

# Structural Properties of Entailment with Proof Terms

  • Reflexivity/Variable rule:

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

  • Transitivity/Substitution

Γ,x:A,ΓN:BΓM:AΓ,Γ[M/x]N:B(T/S)\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 AA, then x:Ax:A is no longer needed. We can substitute xx with MM in the proof NN of BB.

  • Weakening:

ΓM:AΓ,ΓM:A(W)\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:Ax:A,y:A,then we can pick one of them z=xz=x or z=yz=y and substitute the other one with zz:

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

  • Exchange:

Γ,x:A,y:B,ΓN:CΓ,y:B,x:A,ΓN:C(X)\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:

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

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

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

  • Conjunction Elimination:

ΓM:ABΓfst(M):A(E1)ΓM:ABΓsnd(M):B(E2)\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 xx as a variable:

Γ,x:AM:BΓλx.M:AB\cfrac{\Gamma,x:A\vdash M:B}{\Gamma\vdash \lambda x.M:A\supset B}

  • Implication Elimination:

ΓM:ABΓN:AΓM(N):B(E)\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:AM:A,M':A are the same. We denote it as MM:AM\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 MM:AM\equiv M':A, then that their images under any operator should be equivalent. In
other words, we should be able to replace MM with MM' everywhere. For example, it shoule be true that:

ΓMM:ABΓfst(M)fst(M):A\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 MM:AM\equiv' M':A implies MM:AM\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:

ΓM:AΓN:BΓfst(M,N)M:AB(β1)ΓM:AΓN:BΓsnd(M,N)N:AB(β2)\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:

Γ,x:AM:BΓN:AΓ(λx.M)(N)[N/x]M:B(β)\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:

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

Conjunction:

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

Implication:

ΓM:ABΓMλx.M(x):AB(η)\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
ABA\wedge B A×BA\times B
ABA\supset B ABA\rightarrow B or BAB^A
\perp 0
ABA\vee B A+BA+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 ABA\leq B when
AA implies BB.
However, we now wish to keep track of proofs, so if MM
is a proof from AA to BB, we want to think it as a map
M:ABM:A\rightarrow B.

Identity map:

id:AAid:A\rightarrow A

Composition:
We should be able to compose maps:

f:ABg:BCgf:AC\cfrac{f:A\rightarrow B\quad g:B\rightarrow C}{g\circ f:A\rightarrow C}

Coherence Conditions:

idBf=f:ABfidA=f:ABh(gf)=(hg)f:ADid_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 AA there is a unique map A1A\rightarrow 1. This corresponds to \top being the greatest object in a Heyting Algebra, meaning that for all AA, A1A\leq 1.

Existence:

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

Uniqueness:

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

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

1

where the diagram commutes.

First, the existence condition means that there are maps:

fst:A×BAsnd:A×BBfst:A\times B\rightarrow A\\ snd:A\times B\rightarrow B

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

M:DAN:DBM,N:DA×B\cfrac{M:D\rightarrow A\quad N:D\rightarrow B}{\langle M,N\rangle:D\rightarrow A\times B}

and the diagram commutes meaning

fstM,N=M:DAsndM,N=N:DBfst\circ\langle M,N\rangle=M:D\rightarrow A\\ snd\circ\langle M,N\rangle=N:D\rightarrow B

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

P:DA×BfstP=M:DAsndP:DBP=M,N:DA×B\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, fstP,sndP=P\langle fst\circ P,snd\circ P\rangle=P.

Another way to say above is:

fst,snd=idM,NP=MP,NP\langle fst,snd\rangle=id\\ \langle M,N\rangle\circ P=\langle M\circ P,N\circ P\rangle

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

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

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

ap(λ(h)×idA)=h:C×ABap\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 λ(h)×idA=λ(h)fst,snd\lambda(h)\times id_A=\langle \lambda(h)\circ fst,snd\rangle.\
The map λ(h):CBA\lambda(h):C\rightarrow B^A is unique, meaning that

ap(g×idA)=h:C×ABg=λ(h):CBA(η)\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:

1:fstM,NM2:sndM,NN1:(λx.M)(N)[N/x]M1:case(inl(M);x.P,y.Q)[M/x]P2:case(inr(M);x.P,y.Q)[M/y]Q\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)case(x;y,z) means if x then y else z. inl(M)inl(M) means that in
the proof MM, we use the left proof x:Px:P and 1\vee_1 to prove PQP\vee Q.

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

Recall the η\eta rules we have given so far:
Truth:

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

Conjunction:

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

Implication:

ΓM:ABΓMλx.M(x):AB(η)\cfrac{\Gamma\vdash M:A\supset B}{\Gamma\vdash M\equiv\lambda x.M(x):A\supset B}(\eta\supset)

Edited on Views times