[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

[Andrej Bauer]

> Sorry but I don't really understand Andrej and Mathieu's last mails. In
> size-based termination, there is no ordinal in the type system itself.
> Ordinals are just used in the meta-theory to justify that, indeed, every
> well typed term terminates.

I was just pointing out that well-founded relations are the correct
notion to use.

Ordinals require classical logic so you'll burn when you try to bring
measures of termination from meta-theory down to theory. For instance,
what happens if you want to formalize the meta-theory? You can only
sensibly formalize ordinals if you have excluded middle, otherwise
they get weird.

Ordinals are well-founded and *linear*, and there will be cases where
the well-founded part is readily available, but the linearity
requirement just gets in the way. Since linearity is not needed to
show termination, why would we insist on it? For instance, if we want
an automated tool for proving termination, why bother with linearity
when all we need is well-foundedness? (Does Agda termination checker
use ordinals?)

So I really do not see an advantage to using ordinals, except perhaps
easy notation. But I am not actually ruling out ordinals, I am just
saying that we should use the more general well-founded relations, so
the ordinal notations are still there for those cases where they are
the best thing to use.

With kind regards,

Andrej