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).
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.