Remove postulates

[fredrik-bakke]

With #1373 I began work towards removing axioms as postulates in the library, this has multiple benefits as well as drawbacks. The current proposal does not make any changes to the body of any file (i.e. the code after the imports section) except for fundamental files that directly interfaces with Agda through BUILTIN pragmas, their dependencies, and the files about the axioms themselves.

Pros

• It enables axiom analysis such as reverse mathematics. For instance, we can formally establish that univalence implies function extensionality. We currently have a "formal" proof of this fact in the library, but it relies on an external (nonformal) tool to verify that no part of that proof applies any other axiom than univalence. Alternatively, the reader must verify manually that no part of the proof relies on any other axiom.
• We can have developments of mutually inconsistent foundational theories in the library.
• Lowers the barrier between TypeTopology formalizations and agda-unimath formalizations.
• Potentially makes it possible to reenable the --safe pragma for most of the library.

Cons

• Requires more bookkeeping. If a module depends on function extensionality, we must state so explicitly with

  open import foundation.function-extensionality-axiom
  open import foundation.truncations
  
  module
    namespace.modulename
      ( funext : function-extensionality)
      ( truncations : truncations-exist) 
    where

  and must pass on these axioms to every dependency that also need these, e.g.

  open import namespace.other-module1 funext
  open import namespace.other-module2 funext truncations
  open import namespace.other-module3
  open import namespace.other-module4 truncations

  The dependency resolution here could potentially be partially automated.

• Using the above approach, the granularity of the axiom analysis is limited to a per-file basis. This may be insufficient for certain formalizations, lest one wishes to split certain files into more files.

• For custom $\beta$-rules it is necessary to use postulates. Therefore, even after depostulating colimits, we will need to maintain postulates for the corresponding strict computation rules to work.

Work items

The following work items are organized such that each "depostulate" step is almost entirely automated.

• Create separate files for each axiom statement, without consequences.
• Factor files with BUILTIN pragmas to not depend on any axiom.
• Write script to generate new axiom dependencies.
• Depostulate funext
• Depostulate univalence
• Depostulate truncations
• Depostulate replacement
• Depostulate colimits
• Depostulate extensionality of coinductives
• Depostulate modal type theory
• Update documentation

[fredrik-bakke]

For depostulating truncations and colimits, some further work is required to be able to state the axioms without having dependencies on function extensionality or univalence. Ideally, we would phrase the existence of truncations as asking that the global subuniverse of truncated types is reflective.

[fredrik-bakke]

Also, for files that depend on univalence, we should consider applying the module univalence-implies-function-extensionality so that we don't have to maintain funext as a second hypothesis.

[VojtechStep]

so that we don't have to maintain funext as a second hypothesis

Coming back to this, univalence gives you function-extensionality-Level l l, not function-extensionality-Level l1 l2, AFAIK. Is that incorrect, or do you propose removing the second hypothesis from modules which only need extensionality of maps with domain and codomain in the same universe?

[fredrik-bakke]

so that we don't have to maintain funext as a second hypothesis

Coming back to this, univalence gives you function-extensionality-Level l l, not function-extensionality-Level l1 l2, AFAIK. Is that incorrect, or do you propose removing the second hypothesis from modules which only need extensionality of maps with domain and codomain in the same universe?

That's incorrect https://martinescardo.github.io/TypeTopology/MGS.FunExt-from-Univalence.html#786

[fredrik-bakke]

Sorry, the cited formalization entry isn't homotopy coherent. This one is though: https://martinescardo.github.io/TypeTopology/MGS.FunExt-from-Univalence.html#5425

EDIT: and the one directly above it

[fredrik-bakke]

So it will give us univalence-axiom -> function-extensionality, i.e. the implication for the statements universally quantified over all universe levels, which is what I'd propose we use.

[VojtechStep]

Oh nice, so it's just our current formalization which could be more general 👌