Various new theorems in constructive univalent mathematics written in Agda Tested with the development version 2.6.0 of Agda. Martin Escardo, 2010-- Continuously evolving. https://github.com/martinescardo/TypeTopology A module dependency graph (updated manually from time to time) is available at https://www.cs.bham.ac.uk/~mhe/agda-new/dependency-graph.pdf Clickable index: \begin{code} {-# OPTIONS --without-K --exact-split #-} import SafeModulesIndex import UnsafeModulesIndex \end{code} There are only three, periferal, unsafe modules. One of them is to get a contradiction from type-in-type. The other two assume (meta-theoretically) the Brouwerian axiom "all functions are continuous" to prove a countable Tychonoff theorem and a form of the compactness of the Cantor type/space. Most modules rely on concepts and ingredients from univalent mathematics. However, instead of postulating these non-existing ingredients, we take them as assumptions (for single definitions/construction/theorems/proofs or for whole modules via module parameters). These ingredients do exist in the new cubical Agda, and we intend to eventually port this development to cubical Agda. The only obstacle at the moment is that there is no pattern matching on refl at present in cubical Agda, and hence we would need to rewrite large portions of the code here to use J rather than pattern matching on refl.