## 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}$$

## Materials

### Lecture Note

HoTTEST_Lecture_1.pdf