[Agda] Re: Relaxing the strict positivity requirement
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