[Agda] Re: Relaxing the strict positivity requirement

[Abhishek Anand]

I have a related question below. Thanks!

Peter Hancock <hancock at ...> writes:

> 
> As for a type-theoretic notion of ordinal, one can use induction recursion 
to
> define sets whose elements are trees with ordinal-like properties, with
> enormous hight (wrt a certain hierarchy of enormity devised by Paul Mahlo).

Have such types with enormous-ordinal-like members been defined somewhere in 
Agda(or a similar formal system with induction-recursion)?


Thanks,
Abhishek