練習問題 4.4.2

逆の等式 
unzip . zipp = id
は成り立つか． 





xsys = ([],y:ys)


と仮定する．


   (unzip . zipp) xsys
=      { (.)，xsys の定義 }
   unzip (zipp ([],y:ys))
=      { zipp の定義 }
   unzip (uncurry zip ([],y:ys))
=      { uncurry の定義 }
   unzip (zip [] (y:ys))
=      { zip の定義 }
   unzip []
=      { unzip の定義 }
   pair (map fst, map snd) []
=      { pair の定義 }
   (map fst [], map snd [])
=      { map の定義 }
   ([],[])

明らかに

([],[]) ≠ ([],y:ys) ＝ xys

であるから，

unzip . zipp = id

は成り立たない．