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
Though 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
Record on Youtube
It's actually judgmentally equal, ref.