Translating from agda

Stream: general

[Tibor Bjornam]

Hello. I have written a little piece of code in agda, but I'd like to continue in lean to see its capabilities. Sadly, I don't know much of it yet and so the rewriting of the aforementioned code has stuck. Would some of you help me with this, so that I can see and catch on peculiarities of developing proofs in lean?

https://gist.github.com/insignia-magnum/f4e90b87102ed0c308ca8a8950aa9586

[Reid Barton]

Lean doesn't support induction-recursion, and (if I understand what you're doing correctly) can't prove the existence of a U like this without additional axioms (existence of inaccessible cardinals).

[Mario Carneiro]

Actually, in this particular case I think it is possible to prove the existence of U, because every set constructed by F[_] is finite