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.
Revision on March 12, 2016 at 03:30:50 by
Marc Bezem?.
See the history of this page for a list of all contributions to it.