[the_french]

This is an interesting idea but is there any description of the soundness of this approach? Any functionality capable of subsuming not just inductive types but higher-inductive types is going to be very subtle. I looked around on the repository but I can't find any formal description of the language or type theory, which is worrying for a proof tool.

[skybrian]

The plan for Kind itself seems to be to allow possibly unsound expressions (for example that don’t terminate), but to have consistency checkers. See:

https://github.com/kind-lang/Kind/blob/master/CONTRIBUTE.md#...

[logicchains]

There's a paper on the soundness of self types: https://homepage.divms.uiowa.edu/~astump/papers/fu-stump-rta...