Formalize asserted connections between postulates in design principles

[fredrik-bakke]

The following is an excerpt from DESIGN-PRINCIPLES.md:

Note that there is some redundancy in the postulates we assume. For example, the univalence axiom implies function extensionality, but we still assume function extensionality separately. Furthermore, The interval type is contractible, so there is no need at all to postulate it. The circle can be constructed as the type of ℤ-torsors, and the replacement axiom can be used to prove there is a circle in UU lzero. Adittionally, the replacement axiom can be proven by the join construction, which only uses pushouts. Finally, the Agda built-in types do not change the semantics of the theory, they only give convenience to the user of the library.

It would be nice if most of these assertions were formalized in the library and linked to from the design principles.

Concretely, the following statements can be formalized:

• [ ] The circle can be constructed as the type of ℤ-torsors.
• [ ] The replacement axiom can be used to prove there is a circle in UU lzero.
• [ ] The replacement axiom can be proven by the join construction. (This is Theorem 4.6 of Egbert's article The join construction (arXiv:1701.07538))