# Homotopy Type Theory (LMFI)

## Lecture 1: J eliminator, Truncation, Extensional type theory

Correspondence between Types and Topological spaces

Recall that

## Lecture 3: Inductive/co-Inductive types

Examples of inductive types:

Streams:

## Lecture 5: Higher Inductive Types

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

μ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

Globular Sets