Fix levels of universes

mmontin / libndt

A formal library on spreadable properties over linked nested datatypes

0 stars 1 forks source link

Fix levels of universes #6

Open mmontin opened 2 years ago

mmontin commented 2 years ago

We need to gain some genericity in the newest versions of our work. There are two options:

either go back to setw, but that's questionable whether or not that's even possible
or just use and additional level parameters spread throughout the library

pedagand commented 2 years ago

Concerning the first point, my worry is that we will have to compose the functors in Set\omega with Applicative functors, which may not happily live in Set\omega.

Concretely: one should start from #2, reintroduce Set\omega and see whether that can be fixed or understand what is broken.

pedagand commented 2 years ago

@mmontin would you mind taking over this one?