Weird exercise #17
Description
There is Exercise 5 in the "Propositions and sets" section:
Exercise 5: Prove that \Sigma (x : A) (B x) preserves propositions.
But the logic of propositions is not closed under sigmas as it's written down in the tutorial. This exercise is either poorly formulated or it's just incorrect. In either case, it's rather confusing and misleading.