I'm still amazed by these kind of solutions and each time I wonder : "Is this person a thousand times more clever than the rest of us? Or does he/she spends 4 * time on the problem studying its ins and outs in order to find the most compact and obscure algorithm..."

But that was for bonus points.

For the ranking, that should not have been optional really.

No, it's fixed in the final test.

I think the problem is still not fixed. You might want to import a definition of ≡ in the test code.

The random tests incorrectly expect it to be possible to delete a class attribute from an instance. On a normal Python class, this raises an AttributeError. Solutions that preserve this normal behavior should be accepted.

Am I the only one who followed the directions and wrote an infinite stream (up to integer precision) rather than sieving to a predefined limit?

Someone explain this magic pls :o

Thank you for suggestion.
Fixed

Agda test cases should not open the solution; that can often be exploited to bring unexpected definitions into scope.

Can someone please explain this? (I'm mostly curious about the last line.)

Fixed

Before I could start coding, I had to manually concatenate the preloaded snippets interspersed through the description and hunt down some missing imports. Please make the preloaded part directly copy+pasteable and/or uncommentable.

Thanks for the info. Changed the description and tests.

From Preloaded:

-- Cartesian powers of ℕ. Zeroth power is nonsense.
ℕ×ℕ^ : ℕ → Set
ℕ×ℕ^ zero = ℕ
ℕ×ℕ^ (suc n) = ℕ × ℕ×ℕ^ n

The zeroth power is not nonsense; it serves as a base case in the natural definition

ℕ^ : ℕ → Set
ℕ^ zero = ⊤
ℕ^ (suc n) = ℕ × ℕ^ n

and falls out automatically from the other natural definition

ℕ^ : ℕ → Set
ℕ^ n = Fin n → ℕ

Of course, task 2 would then need to change to ℕ ⇔ ℕ^ (suc n).