ERRATA FIRST EDITION:

Page 108: The definitions of predicates and power types are not correct.

Page 115: Mere propositions are empty or equivalent to a point, but not equal.

Page 120: At the end of the section the alternative characterisation of equivalence is not correct. It must involve left and right "inverses" which are inverse up to homotopies.

The reference [Mueller-Stach2025] concerning Emmy Noether is likely to appear 2027 or 2028. It is freely available at the author's homepage.