Refactor universal property of suspensions

[fredrik-bakke]

Refactors universal properties of suspensions to use the Level-naming scheme.

[EgbertRijke]

Wouldn't it be better convert to stating universal properties in UUomega only? I don't really know what the level-wise universal properties are good for

[fredrik-bakke]

Wouldn't it be better convert to stating universal properties in UUomega only? I don't really know what the level-wise universal properties are good for

Backward compatibility, I suppose.

[fredrik-bakke]

Also, sometimes it is used in Sigma types. E.g.

  universal-property-pushout-extension-by-equivalences :
    {l : Level} → is-equiv i → is-equiv j → is-equiv k →
    Σ (cocone f' g' X) (λ d → universal-property-pushout-Level f' g' d l)

[EgbertRijke]

Reference in new issue

Ah, your point is here. That code doesn't look very good to me. Looks like I have another refactoring job to do.

[EgbertRijke]

Wait I think I am already doing that refactoring in #885. Mind you I might have been addressing some of these universal properties there too.

[fredrik-bakke]

Wait I think I am already doing that refactoring in #885. Mind you I might have been addressing some of these universal properties there too.

Oh no. I was working on that right now

[EgbertRijke]

I think #885 is already much deeper in than you are here. Since this pr is <200 lines of code, perhaps it would be better to abandon this one. I'm really sorry.

[fredrik-bakke]

Well, 200 LOC is what I've pushed...

[fredrik-bakke]

Also, there doesn't seem to be any overlap in what I've actually pushed. Am I missing something?

[fredrik-bakke]

I decided to just ignore the up problem for now, as it seems to be a more delicate problem than I first anticipated.