Homotopy Theory

Speaker: Hugo Bacard (Western)

"Identity types and higher groupoids"

Time: 14:00

Room: MC 107

After recalling the construction of identity types as inductive types, we will use the induction principle to prove basic facts about identity types. Throughout the talk, we will pursue the analogy between identity types and path spaces. We will illustrate how iterated identity types form a structure reminiscent of the low-dimensional data of an $\infty$-groupoid.