Let \(U\) be a universe and let \(X\) be a \(U\)-topos. If \(A\) is a construction in the category of types, then we write \(A\mathrel {@}X\) for the same construction but performed in the category of sheaves on \(X\).
Let \(U\) be a universe and let \(X\) be a \(U\)-topos. If \(A\) is a construction in the category of types, then we write \(A\mathrel {@}X\) for the same construction but performed in the category of sheaves on \(X\).