Let \(U\) be a universe, let \(V\) be a universe strictly greater than \(U\), and let \(X\) be a \(U\)-topos. Then we have a canonical equivalence
Let \(U\) be a universe, let \(V\) be a universe strictly greater than \(U\), and let \(X\) be a \(U\)-topos. Then we have a canonical equivalence