I guess the answers to my questions lie in HoTT book section 5.4.

This Kata is not compatible with Lean 3.20.c as of 08/10/2020

Reset my assessment to 8 kyu. Changed estimated rank to the lowest possible one -- 5 kyu. Approved to the lowest possible rank -- 5 kyu. Idk if it can be made to 6 kyu tbh

Done

Done

Note to moderators: This Kata is not yet ready for re-approval - its average assessed rank must be at most 6 kyu before it can be considered for re-approval. See https://github.com/codewars/codewars.com/wiki/Agda-Kata-that-require-rank-adjustment for more details.

Note to moderators: This Kata is not yet ready for re-approval - its average assessed rank must be at most 5 kyu before it can be considered for re-approval. See https://github.com/codewars/codewars.com/wiki/Agda-Kata-that-require-rank-adjustment for more details.

Approved

Lean Translation Kumited - please accept :-D

i changed my rating to 8kyu which seems to have made 7kyu possible

Note to moderators: This Kata is not yet ready for re-approval. Its current average assessed rank is 6 kyu but we need to bring it down to at most 7 kyu before it can be considered for re-approval.

See: Codewars/codewars.com#2001

Thanks, fixed.

Reasonable, the kata is now fixed.