[Agda] Re: Relaxing the strict positivity requirement

Abhishek Anand abhishek.anand.iitg at gmail.com
Tue Nov 19 06:10:43 CET 2013

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 
> 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)?


More information about the Agda mailing list