Natural deduction

Trivial, not necessary to say too much here.

Simple typed lambda calculus (STλC or STLC)

Still trivial, just need to clarify some notations the teacher is using.

$pr_1 (p, q)$ means take the first element out from pair $(p, q)$, which is always write as $(p, q).1$, eg.

$$ \require{bussproofs} \begin{prooftree} \AxiomC{p: P} \AxiomC{q: Q} \BinaryInfC{$pr_1 (p, q) \doteq p: P$} \end{prooftree} $$

Here $\doteq$ is by definition equal1, which I always use $\equiv$.

Dependent type theory

Tough I had some basic knowledge of this before (eg. Dependent types can be viewed as predicates due to Curry-Howard Corresponding), but I do learned some more.

The meaning of the word "dependent"

I used to understand this in an intuitive way, in the class the teacher introduced a semi-formal definition of "dependent", ie. the items on the right side of $\vdash$ depends on those on the left side.

Rules of π-types

$$ \Pi-form: \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma ,x:P \vdash Q\ type$} \UnaryInfC{$\Gamma \vdash \Pi_{(x:P)} Q\ type$} \end{prooftree} $$

$$ \Pi-intro: \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma ,x:P \vdash q:Q$} \UnaryInfC{$\Gamma \vdash \lambda x.q: \Pi_{(x:P)} Q$} \end{prooftree} $$

$$ \Pi-elim: \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma \vdash f:\Pi_{(x:P)} Q$} \AxiomC{$\Gamma \vdash p:P$} \BinaryInfC{$\Gamma \vdash f\ p:Q[p/x]$} \end{prooftree} $$

$$ \Pi-comp-\beta: \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma ,x:P \vdash q:Q$} \AxiomC{$\Gamma \vdash p:P$} \BinaryInfC{$\Gamma \vdash (\lambda x.q) p \doteq q[p/x]:Q[p/x]$} \end{prooftree} $$

$$ \Pi-comp-\eta: \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma \vdash f:\Pi_{x:P} Q$} \UnaryInfC{$\Gamma \vdash \lambda x.f\ x\doteq f:\Pi_{(x:P)} Q$} \end{prooftree} $$


Lecture Note


Record on Youtube


It's actually judgmentally equal, ref.