cleanup in FinNat

[Alizter]

We had a lot of universes being generated here, I've cut them down a bit by using Universe Minimization ToSet.

[jdchristensen]

Are the Monomorphic modifiers still needed?

(Also, I don't get why there are various path_* lemmas like path_zero_finnat which are just aliases for path_ishprop. Can't path_ishprop just be used?)

[jdchristensen]

I got rid of the unneed path_*_finnat definitions, and adapted path_succ_finnat to fit better what is needed. I also simplified a couple of proofs. I suspect finnat_ind could be made to compute better.

I also got rid of one unneeded universe variable in finnat_ind, and annotated a few things to enforce that universe variables don't accidentally arise again.

I didn't think about why some things are marked Monomorphic. Can we just get rid of that?

[Alizter]

@jdchristensen I think that was misused to get things to not be polymorphic, but that's already the case when we have no Univ variables, therefore it's fine to remove.

I also had some patches cleaning up things here similarly to what you did, but I'll need to check in detail later as I may have changed some proofs differently.

[jdchristensen]

Ok, I removed Monomorphic. We still use it in other places, e.g. things like Funext are marked as monomorphic even though they don't take any universe variables. I'm not sure what advantage adding Monomorphic gives if something already doesn't use any universe variables, but maybe there's some tiny speedup from this?

[jdchristensen]

PS: Sorry if I interfered with other patches you had queued up!

[Alizter]

Ok, I removed Monomorphic. We still use it in other places, e.g. things like Funext are marked as monomorphic even though they don't take any universe variables. I'm not sure what advantage adding Monomorphic gives if something already doesn't use any universe variables, but maybe there's some tiny speedup from this?

I am not sure if there is a speed up, but its probably not worth confusing readers.

PS: Sorry if I interfered with other patches you had queued up!

No worries, I've pushed some of the changes I was going to do while we were here.

[jdchristensen]

This looks good to me, modulo the build error and the one comment about succ_finnat.

[Alizter]

I've fixed the universe issue in 8.19 (for some reason idpath wasn't being minimized to idpath@{Set} and I've reverted the removal of path_succ_finnat like you suggested.