[Agda] nontermination and Sized types

[Andrew M. Pitts]

> On 2 Oct 2020, at 13:36, vlad <Vlad.Rusu at inria.fr> wrote:
> 
> Looking at (V2) one can notice that nonterminating'  looks like a well-founded induction principle for the _<_ relation on Size, defined by j < i iff (t : Size< i). Which is strange since _<_ is *not* well founded, as ∞ < ∞ holds. Indeed, if nonterminating' were accepted then it could be used to prove that _<_ is  well  founded: just take P s = "there is no infinite <-decreasing sequance starting at s". So, I believe the Agda termination checker rightfully rejects the definition (V2). 

I believe issue #3026 is still open and that at the moment (v2.6.1) Agda allows one to prove _<_ for Size is well-founded and hence derive a logical inconsistency. :-)

Andy