Experiment: depostulating univalence

[EgbertRijke]

This is an experiment

The motivation for this PR is merely that I am curious what the library will look like if we wouldn't have postulates.

This pull request is not to be considered for merging.

[fredrik-bakke]

Hey! I'm excited to see you're experimenting with this. Have you looked at the following approach to depostulating axioms?

In the file foundation.univalence, to assume the univalence axiom, we import foundation-core.univalence and then assume the axiom as a module parameter for the entire file by declaring the top-level module with

open import foundation-core.univalence

module foundation.univalence (univalence : univalence-axiom) where

Elsewhere, when we select to import this module, we can also start by assuming univalence for the entire file by declaring the top-level module with

open import foundation-core.univalence

module elsewhere (univalence : univalence-axiom) where

and then opening foundation.univalence and passing univalence to it:

open import foundation.univalence (univalence)

EDIT: The benefit here is that we can forget the distinction between whether univalence is a postulate or a parameter for the remainder of the file.

One can also open import foundation.univalence without passing the parameter, but it's not clear to me what that means. EDIT: presumably one will have to pass univalence whenever one invokes an entry from that module in this case.

[EgbertRijke]

As far as I got until now, there was no point where I wanted to assume univalence for an entire file. I am also not quite sure if I fully understand why we would want to do that.

As I understood it, the point of depostulating univalence would be that we mark precisely all entries that rely on univalence. But then assuming univalence for an entire file seems to defeat that purpose. Perhaps I am misunderstanding something.

[fredrik-bakke]

As far as I got until now, there was no point where I wanted to assume univalence for an entire file. I am also not quite sure if I fully understand why we would want to do that.

As I understood it, the point of depostulating univalence would be that we mark precisely all entries that rely on univalence. But then assuming univalence for an entire file seems to defeat that purpose. Perhaps I am misunderstanding something.

The way I see it, the approach I suggested "gives the best of both worlds". On the one hand, it minimizes the code overhead of not having certain axioms postulated for the entire library, since you can just assume them for the entire file and then forget about them. On the other hand, it enables the possibility to be more granular about when axioms are invoked, if one does not assume them file-wide.

To my understanding, that is the benefit of depostulating axioms. It doesn't quite sound like a universal benefit to me to have to pass them around everywhere, although that certainly gives us more control which is desirable in some scenarios.

Perhaps univalence is not the best example because there aren't that many files where we apply univalence all over the place. I would guess function extensionality would demonstrate my point more clearly.

Maybe I am misunderstanding you. If you are of the opinion that the postulated axioms are used so rarely that it doesn't make sense to use them as top-level module parameters because that would usually be unwarranted, and be warranted so rarely that when it happens it confuses readers, then that's something I haven't considered in great detail yet.