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).
Find the term ac on slide 21 of HoTT.pdf HoTT.pdf.
Do Exercise 1.1 and 1.2 of the HoTT book 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.
16 March
As to Exercises 1.7 and 1.14, give the -type and prove for all that for all .
Do Exercises 2.1 - 2.4 in the HoTT book.
Revision on March 16, 2016 at 01:54:47 by
Marc Bezem?.
See the history of this page for a list of all contributions to it.