Well they claim it is a HoTT (thus presumably univalent) and furthermore has higher inductive types, neither of which exist in Coq's CIC. For example, they emp

Well they claim it is a HoTT (thus presumably univalent) and furthermore has higher inductive types, neither of which exist in Coq's CIC. For example, they emphasise that function extensionality is a theorem here: https://arend-lang.github.io/about/arend-features https://arend-lang.github.io/about/arend-features (not true in CIC). It would just be nice to see a list of the rules. Still I don't want to get hung up on this; the rules must exist somewhere and presumably will become more discoverable. The project looks superb.