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

Showing changes from revision #2 to #3: Added | ~~Removed~~ | ~~Chan~~ged

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 is an equivalence relation for all types A
2. Untyped $\lambda$ -calculus: maximally reduce (+ 1 2) and (* 3 0)
3. Maximally reduce (+ 0 x) and (+ x 0). Is there a difference?

Revision on March 1, 2016 at 03:44:17 by Marc Bezem?. See the history of this page for a list of all contributions to it.