Ayhon @ayhon@qoto.org

@CapitalB @531095 @camwilson I think they mean that users which normally went to Wikipedia now instead go to these AI tools for that information. Therefore, they're "stealing" traffic.

@sophiajt Where you thinking of something along the lines of Unison?

@mra

If I understood correctly from the page, the advantages are purely operational. Cumulative universes seem to be a relaxation to more easily allow the definition of certain functions, and for instance prevents having to implement a function twice, once for the value computation and once for the universe level computation.

So I guess it's used in the HoTT book since it leads to potentially cleaner definitions, but left out of theorem provers since terms having a unique type is desirable.

@mra Aaah, that must have been why I was suggested to talk with Martin Escardo then. Thanks for the link!

@MartinEscardo
I had a question about univalent mathematics and I was told you'd be the one to ask. I hope you don't mind

Reading the HoTT book I noticed that they defined universes to be cumulative. This surprised me because in theorem provers such as Lean and allegedly Agda (I was told), this is not the case. In the book itself they mention a downside of having cumulative universes being that a term no longer has a unique type, but they don't mention any advantages of constructing them this way.

Therefore, my question is: what is the advantage of having cumulative type universes?

@endospore Indeed! I also use neovim and enjoy this behavior a lot

@mustache Usually I'd say caret, but when using vim it's true that the block works better, otherwise actions like `a` look like they skip a character.

I guess my answer comes down to "it depends on the application", which is not very satisfying.

@yosh Any recommendations on where to start?

@lodurel Indeed, I guess I was just questioning the current utility of installing texlive in the first place. Personally the software package has becnisl large that I've chosen to delegate its installation and usage to a third party "in the cloud". Admittedly, I have not yet had to write something as extensive as a PhD thesis, so my situation is different. If I were to do a PhD, I probably would need to have a local installation, and I'd probably not uninstall it until I have to change PCs (and reinstall the OS with it)

@lodurel Honestly, I don't even have Tex installed. If I need to do something that I can't get down with Markdown, I go to Overleaf.

I have videogames installed which take less space than texlive