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.
There is Exercise 5 in the "Propositions and sets" section:
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.