Wow, I am delighted to see this!

However I cannot find a precise reference for the chosen type theory.

E.g., is univalence a theorem in their type theory? I presume it is given that they say their language has "syntax similar to cubical type theory" but I could not say for sure.

What I'm looking for is a reference containing the actual typing rules, like this one for Coq: https://coq.inria.fr/refman/language/cic.html#typing-rules

rather than the syntax of the language used for building these terms.