Some errors and other things I noticed

[abuseofnotation]

Quest 0

At "Part 1 - False / Empty / Initial object"
https://thehottgameguide.readthedocs.io/en/latest/0-trinitarianism/quest-0.html

The proof of explosion is not given and explained. How would we know about ()? The exercise cannot be completed.

Quest 2

At "A Tautology / Currying / Cartesian Closed"
https://thehottgameguide.readthedocs.io/en/latest/0-trinitarianism/quest-2-side.html

The link to adjunction is dead.

The file
https://github.com/thehottgame/TheHoTTGame/blob/main/0Trinitarianism/Quest1.agda

actually contains tasks from Quest 2

https://thehottgameguide.readthedocs.io/en/latest/0-trinitarianism/quest-2.html#part-0-existence-dependent-pair-total-space-of-bundles

In

https://thehottgameguide.readthedocs.io/en/latest/0-trinitarianism/quest-3.html

"More generally given A : Type and B : A → Type we can form the pi type (x : A) → B x : Type (in other languages Π (x : ℕ), isEven n), with interpretations :"

There is a copy-paste error in the last statement, it has the "isEven" function)

Quest3

No specific error, but I had a lot of issues here
https://thehottgameguide.readthedocs.io/en/latest/0-trinitarianism/quest-3-side.html#decidability-of-iseven

I couldn't get this line, even after looking it up.

isEvenDecidable (suc zero) = right (λ ())

Quest 4

In

https://thehottgameguide.readthedocs.io/en/latest/0-trinitarianism/quest-4.html

the tip saying "If you are tired of writing {A : Type} {x y : A} each time you can stick..." should be above the exercise, as the task as it is doesn't work if it is pasted