Homotopy Type Theory HoTT Mini-Course > history (Rev #4, changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

HoTT Mini-Course at CMU

Marc Bezem, Spring Semester 2016

Place and Time

• 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

Resources

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

Homework

• 2 March
  1. Prove that Eq_A on slide 2 of DTUA.pdf is an equivalence relation for all types A A.
  2. Untyped $\lambda$ -calculus: maximally reduce (+ 1 2) and (* 3 0) 0).
  3. Maximally reduce (+ 0 x) and (+ x 0). Is there a difference?
• 7 March
  1. 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).
  2. Same task as previous, but now with Eq_A from slide 8 of DTUA.pdf (now they are all provable).
  3. Read the Introduction of the HoTT book.