The document is slightly outdated. We do not have the rule iso A B (λx ⇒ x) (λx ⇒ x) idp idp i ⇒β A in the actual implementation since univalence is true even without it. This rule has another problem. It seems that the theory as presented in the document introduces a quasi-equivalence between A = B and Equiv A B, which means that there are some true statements which are not provable in it. The theory without this rule should be completely equivalent to the ordinary HoTT, even though I cannot prove this yet.
There is a bit more subtlety here than is evident from the brief
description, since everything has to happen in an arbitrary slice
category of the model category. But although the slices of a
cartesian model category are not in general again cartesian, they are
enriched model categories over the base, and so I think I agree that
this works since I lives in the base.
However, section 2.2 of https://valis.github.io/doc.pdf also appears
to assert that an equivalence can be made into a line in the universe
for which coercing along the line is *definitionally* equal to the
action of the given equivalence, and such that the line associated to
the identity equivalence is definitionally constant. The latter seems
like it might be obtainable by a lifting property, but I don't
immediately see how to obtain the former in a model category?