With the operation |=|, any 2 natural numbers are equal and I can prove the following:

p :: Equal (S Z) (S (S Z))
p = NumS NumZ |=| NumS (NumS NumZ)

I am new to Haskell, but I do not understand how |=| compiles

I mean you need up to sqrt(n)+1 no n/2+1

You are looping over much more integers than needed

Both algorithms are linear on the input; but yes, this one is faster

The sample test for laziness is calling foldr instead of fixFoldr in Haskell

I am new in Haskell and I do not know how to use the type

type Lens s t a b = forall f . Functor f => (a -> f b) -> (s -> f t)

Any pointers or link to a tutorial on how to instanciate certain functor f?

When the test asks for the page number of the item element at -1, it expect Just 0; in Haskell

Why sort in this solution?

I thought of the same :)