Martin Hyland classified the exponentiable locales as the locally compact ones. This chapter proves the counterpart of Hyland's result for inductively generated formal topologies. More precisely, by adapting Hyland's proofs to the context of formal topology, it proves that locally compact formal covers are the exponentiable objects in the category of inductively generated formal covers. Then, it deduces the analogous result for inductively generated formal topologies (that is, formal topologies with a unary positivity predicate). This demonstrates once more how impredicative reasoning can be unwound predicatively with great patience, but with the benefit of a quite explicit proof.
Predicative exponentiation of locally compact formal topologies over inductively generated ones
MAIETTI, MARIA EMILIA
2005
Abstract
Martin Hyland classified the exponentiable locales as the locally compact ones. This chapter proves the counterpart of Hyland's result for inductively generated formal topologies. More precisely, by adapting Hyland's proofs to the context of formal topology, it proves that locally compact formal covers are the exponentiable objects in the category of inductively generated formal covers. Then, it deduces the analogous result for inductively generated formal topologies (that is, formal topologies with a unary positivity predicate). This demonstrates once more how impredicative reasoning can be unwound predicatively with great patience, but with the benefit of a quite explicit proof.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.