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).

That was clearly wrong, so I fixed the test to expect a set with an empty array.

Oops, this version has a bug with a small number of (untested) inputs, see the fixed version.