search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 193 forks source link

drop extra universe in istrunc_sigma #1986

Closed Alizter closed 3 months ago

Alizter commented 3 months ago

This was quite difficult to fix, but I worked it out in the end.

The previous proof was using the generated polymorphic induction principle which is actually less general than what we could be. This meant that we required an extra strictly larger universe for the induction hypothesis to work.

Rewriting the proof using a fixpoint allows us to use the most general version of the "induction principle", i.e. the rules of the underlying fixpoint. This allows us to remain in the same universe, simplifying the universe requirements elsewhere too.

The main motivation for this patch was to reduce the universes in istrunc_vector and now we don't need a superfluous larger universe.

cc @mikeshulman who participated in the corresponding Zulip discussion: https://hott.zulipchat.com/#narrow/stream/228519-general/topic/.E2.9C.94.20Truncation.20level.20of.20sigma.20type

jdchristensen commented 3 months ago

Instead of your approach, you can just change induction to simple_induction', and it goes through with the reduced universe variables. No annotations required.

jdchristensen commented 3 months ago

(By coincidence, I've just been trying the use of fixpoints for list in induction, and it works there too!)

Alizter commented 3 months ago

@jdchristensen I don't understand your suggestion. If I change induction to simple_induction' like you said, I end up having unbound universes. Could you elaborate a bit more?

jdchristensen commented 3 months ago

If you completely revert your changes to Types/Sigma.v and just change induction to simple_induction', doesn't it work?

Alizter commented 3 months ago

If you completely revert your changes to Types/Sigma.v and just change induction to simple_induction', doesn't it work?

I tried that, it didn't work for me.

Alizter commented 3 months ago

Ah nevermind, I see the problem. The issue is that I was expecting 3 universes. But your simple induction gives 4, however it is not strictly larger.

jdchristensen commented 3 months ago

? When I use simple_induction', I get istrunc_sigma@{u u0 u1}, with just three universes.

Alizter commented 3 months ago

Oh yes you are correct. I had an annotation left over. Whoops. I will force push the fix.

Alizter commented 3 months ago

Thanks @jdchristensen that is a much cleaner "fix"!