From f6606a8ee6d73850afd7196f87c13ecaf90ec240 Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Sun, 19 Jan 2020 13:32:27 -0500 Subject: [PATCH] added hint to exercise forall-x --- src/plfa/part1/Quantifiers.lagda.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/plfa/part1/Quantifiers.lagda.md b/src/plfa/part1/Quantifiers.lagda.md index 559560ce..ce377716 100644 --- a/src/plfa/part1/Quantifiers.lagda.md +++ b/src/plfa/part1/Quantifiers.lagda.md @@ -121,6 +121,8 @@ data Tri : Set where ``` Let `B` be a type indexed by `Tri`, that is `B : Tri → Set`. Show that `∀ (x : Tri) → B x` is isomorphic to `B aa × B bb × B cc`. +Hint: you will need to postulate a version of extensionality that +works for dependent functions. ## Existentials