"Global" assumptions or axioms (spreading across multiple files)

[fizruk]

Currently Rzk has #assume command (synonymous with #variable and #variables), which introduces local assumptions:

1. assumptions can be used within a section
2. outside the section, assumptions become explicit parameters
3. an Rzk file counts as a section as well
4. implicit use of assumptions is detected by rzk and can be silenced by uses (assumption1 ...) for each definition

Currently, assumptions are used both

• for local parameters in sections (e.g. see #section homotopy-interchange-law)

• for axioms, e.g. in many formalisations we have:

  #assume funext : FunExt
  #assume weakextext : WeakExtExt
  #assume extext : ExtExt
  

However, while we would still like to know which axioms are used in a definition (via uses), it is tiresome to pass them explicitly all the time. To mitigate that, we have several options to adjust Rzk:

1. Add #assume-globally (aka #define-assumption, see Add #define-assumption command #69) that works like #assume, but adds assumptions globally. This leaves #postulate (a command that exists now) for axioms that do not have to be declared in uses and adds simply allows some variables to leave in a "global" section.

2. Use #postulate my-axiom : type for axioms, but adjust uses to also require postulated dependencies to be specified (implicit, but also, maybe, explicit ones). This way we would distinguish local assumptions from axioms in Rzk syntax and so can treat them differently:

   • Local variables only have to appear in uses if they are entirely implicit (do not occur in the type or the body of a definition), whereas axioms should probably always be in uses for clarity.
   • Error messages and hints may be adjusted to be more elaborate depending on whether we have local variable or an axiom.

3. Add new commands to reintroduce assumption or instantiate it:

   • #use section-name.variable would replicate an assumption made previously in section-name and automatically use this assumption when using definitions from section-name AND any section/file that later assumed the same variable; similarly to #assume, the effect of this command would be local to the section;

   • #let section-name.variable := term would automatically use term for all definitions form section-name where variable argument is expected

   Here, #use solves the issue of reusing axioms without extra boilerplate, but also allows to reuse local variables between sections. The suggested version of #let above further allows to partially specialise sections. In fact, this way sections behave like structures, similar to modules. I am not sure this is the correct approach, and, perhaps, a proper module system should be designed and implemented instead. But since this has crossed my mind, I though I'd list it here anyway.

4. Allow (instance) inference for contractible types:

   • use _ for holes (unspecified terms) to be inferred by the proof assistant
   • if the expected type of _ is known, has an inhabitant, and is a proposition, e.g. if the type is FunExt, there is an assumption funext : FunExt and a definition of type is-prop FunExt exists in scope, or if is-contr FunExt exists
   • then automatically use the inhabitant in place of _

   This approach can be useful for many other propositions, not only axioms (e.g. is-segal or is-rezk). But it will not work for axioms that are not propositions (although I can't think of one that would be useful at the moment). This is also a special case of a variant of Agda's instance arguments and could be later extended further.

5. Building up on (4), allow implicit instance arguments:

   • use curly braces for implicit arguments/parameters/assumptions
     { extext : ExtExt}
   • check that ExtExt is a proposition (as in (4)) to allow it to be implicit
   • insert _ automatically when the argument would be given explicit otherwise

   Note that unlike regular implicit arguments, this one does not actually rely on type inference, so should be much easier to add. It also is mostly orthogonal to regular implicit arguments and has to be implemented separately (although, it may benefit from type inference to work in more contexts).

There are probably more ways to deal with axioms. But for now this is the initial list.

From this list, I personally think it makes sense to implement either (2) or (4). (2) is probably much easier to implement and has minimal effect on the language. (4) is probably a more useful feature that is relatively easy to add.

However, I am open to suggestions and comments regarding this.