Maximally reduce (+ 0 x) and (+ x 0). Is there a difference?
7 March
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
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.
14 March
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.
Revision on March 11, 2016 at 17:30:54 by
Marc Bezem?.
See the history of this page for a list of all contributions to it.