I explicitly ignored codata/coinduction as they are complex and rather niche. Even so, they come with their own notion of 'termination' (progress / wfo) and don

I explicitly ignored codata/coinduction as they are complex and rather niche. Even so, they come with their own notion of 'termination' (progress / wfo) and don't magically let you write random non-terminating programs. Depending on what you want to achieve there are plenty of tricks and techniques to encode a divergent program in a sound dependent-type theory, but the best approach to use will depend on the problem statement.