HoTT Mini-Course

- Baker Hall 152
- Monday and Wednesday 13:30 - 16:30
- Exercises 13:30 - 15:00
- Lectures 15:00 -16:30
- We continue during the Spring break
- No lectures 23,28,30 March

- The HoTT book
- Slides The Univalence Axiom in Dependent Type Theory (pdf)
- Slides Homotopy Type Theory (pdf)

- 2 March video
- Prove that Eq_A on slide 2 of DTUA.pdf is an equivalence relation for all types A.
- Untyped $\lambda$-calculus: maximally reduce (+ 1 2) and (* 3 0).
- Maximally reduce (+ 0 x) and (+ x 0). Is there a difference?

- 7 March video
- Let = be Eq_A (slide 2 of DTUA.pdf). Try to prove the groupoid laws on slide 9 of DTUA.pdf (not all are provable, which shows that Leibniz equality is too weak to give types groupoid structure).
- Same task as previous, but now with Eq_A from slide 8 of DTUA.pdf (now they are all provable).
- Read the Introduction of the HoTT book.

- 9 March video
- Find the term
*ac*on slide 21 of HoTT.pdf. - Do Exercise 1.1 and 1.2 of the HoTT book.
- Let
*Bool*be the inductive type with two nullary constructors*false: Bool*and*true: Bool*. Formulate formation, introduction, elimination and computation rules for Bool. - Find a term
*t: U -> U -> Bool -> U*such that*t A B true = A*and*t A B false = B*, for all*A,B: U*.

- Find the term
- 14 March video
- Do as many exercises from Chapter 1 of the HoTT book as you can. You can find some solutions in the HoTT library and by running
`make exercise_solutions.pdf`

after forking the HoTT book on Github.

- Do as many exercises from Chapter 1 of the HoTT book as you can. You can find some solutions in the HoTT library and by running
- 16 March (no video due to connectivity problems)
- As to Exercises 1.7 and 1.14, give the $\Sigma$-type $S$ and prove for all $a:A$ that $(a,refl_a) =_S (x,p)$ for all $x:A, p: a =_A x$.
- Do Exercises 2.1 - 2.4 in the HoTT book.

- 21 March video
- Do Exercises 2.5 - 2.10 in the HoTT book.

- 4 April
- Do as many of the remaining exercises from Chapter 2 of the HoTT book as you can.

- 6 April
- Investigate the action on paths of the function $f : \Sigma A B \to \Sigma A' B'$ given by $g: A\to A'$ and $h: \Pi x:A. B x \to B' (g x)$ in the following canonical way: $f(a,b) = (g a,h a b)$. (Hint: this is a dependent version of a simpler result for Cartesian products).
- Prove that for all $x,y : *$ we have $(x=_*y) \simeq \mathbf{1}$.

category: events

Last revised on September 25, 2018 at 04:48:33. See the history of this page for a list of all contributions to it.