wjzz

{-

$ ghc --make -O0 Boxed.hs 

$ time ./Boxed u 100000000
987459712

real	0m1.034s
user	0m1.028s
sys	0m0.004s

wjzz

{-
  @author: Wojciech Jedynak ([email protected])
-}

{-
2012-03-11

We show that the notions of isomorphism and bijection coincide in type theory.

This follows because from a constructive proof of surjectivity of a function f