From https://rzk-lang.github.io/rzk/v0.6.4/reference/introduction.rzk/#soundness https://rzk-lang.github.io/rzk/v0.6.4/reference/introduction... > rzk-1 assume

From https://rzk-lang.github.io/rzk/v0.6.4/reference/introduction.rzk/#soundness https://rzk-lang.github.io/rzk/v0.6.4/reference/introduction... > rzk-1 assumes "type-in-type", that is U has type U. This is known to make the type system unsound (due to Russell and Curry-style paradoxes), however, it is sometimes considered acceptable in proof assistants. And, since it simplifies implementation, rzk-1 embraces this assumption, at least for now. I do this too (in my HoTT-book-inspired proof-checker)! I do plan on eventually implementing a hierarchy of universes but it doesn't seem to be a problem to let U be of type U. I wonder where the first practical issue comes up when you allow this. --- After writing this comment, I decided to put it up on GitHub. Here is the entire source code of my proof-checker as well as some of the theorems from the HoTT book: https://github.com/sid-code/metalogic/blob/main/dts.org https://github.com/sid-code/metalogic/blob/main/dts.org. It was never meant to be used or even read by anyone else, but here it is. Here is where the universe is defined (unsoundly): https://github.com/sid-code/metalogic/blob/main/dts.org#the-universe https://github.com/sid-code/metalogic/blob/main/dts.org#the-... To see the theorems, scroll down past the machinery to the `(env-define-checked)` calls. Here is the proof that multiplication of natural numbers is associative: https://github.com/sid-code/metalogic/blob/main/dts.org#associativity-of-multiplication https://github.com/sid-code/metalogic/blob/main/dts.org#asso.... There is no type inference, so it's pretty gross. I think it's pretty cool how little you need to actually have a working proof-checker.