Homotopy Type Theory (LMFI)

Lecture 1: J eliminator, Truncation, Extensional type theory

Correspondence between Types and Topological spaces

Lecture 2: Equivalences

Recall that

Lecture 3: Inductive/co-Inductive types

Examples of inductive types:

Lecture 4: Streams

Streams:

Lecture 5: Higher Inductive Types

HIT: Inductive types where equality is also taken into account.

Lecture 6: Encoding of $λ$-calculus, System T & System F

[μC. (C ⟶ C)]

Lecture 7: Category theory in HoTT

We want a notion of category where type is a category, so that there’s a notion of homotopy thanks to model structures.

Lecture 8: Categories in 2-level type theory, Fibrations and co-Fibrations

Category in 2-level type theory

Lecture 8: Cubical type theory

Globular Sets