michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

added hint to exercise forall-x

Browse source
This commit is contained in:
Jeremy Siek 2020-01-19 13:32:27 -05:00
parent ea42753758
commit f6606a8ee6
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/plfa/part1/Quantifiers.lagda.md
View file

@ -121,6 +121,8 @@ data Tri : Set where
``` ```
Let `B` be a type indexed by `Tri`, that is `B : Tri → Set`. 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`. 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 ## Existentials