So what are we actually studying?
- Logic and Proof Theory
- Type Theory
- Category Theory
What's the target? Well there are two.
- The first one is to have enough understanding as to begin learning homotopy type theory.
- The second one is to be able to reason about programs and algorithms, get better at using or constructing features of languages and effectively work on theorem proving (classical and AI).