Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Internal formal topologies in a Heyting pretopos

Madeleine Birchfield (Jan 29 2024 at 18:07):

In order to define a formal topology on an object $A$ inside of a Heyting pretopos $\mathcal{E}$ (i.e. using the internal logic), does the Heyting pretopos have to be an elementary topos?

Jonas Frey (Jan 29 2024 at 19:43):

I don't think so. Isn't the whole point of formal topology to be predicative, by working with bases without completing them to locales?

Jonas Frey (Jan 29 2024 at 19:44):

Anyway, which definition of formal topology are you using?

Mike Shulman (Jan 29 2024 at 20:01):

You might need a $\Pi$-pretopos or a $\Pi W$-pretopos though, depending on the definition and how internal you want it to be.

Andrew Swan (Jan 29 2024 at 20:21):

There's a relevant paper by Van den Berg and Moerdijk at https://arxiv.org/pdf/0912.1242.pdf

Madeleine Birchfield (Jan 29 2024 at 23:09):

It is the cover relation that is the potentially impredicative part of the formal topology, since it is a relation between elements of a formal topology and subsets of the formal topology, so it is unclear how one would internalize such a relation in a Heyting pretopos without power sets.

However, it seems that Ayberk Tosun in his article on formal topology https://odr.chalmers.se/server/api/core/bitstreams/84989823-7398-4eb3-8804-1f88822d1fd2/content provides a definition of a formal topology which does not require the cover relation to be defined, and thus it is predicative. Since Tosun is working in dependent type theory, this implies that formal topologies are definable in any $\Pi W$-pretopos. The cover relation on the formal topology is inductively defined, but it still uses power sets in the article, so that part is still impredicative.

Andrew Swan (Jan 30 2024 at 09:34):

In type theory you can go a long way if you're careful about universe level. E.g. power set is okay predicatively as long as you recognise it belongs to the next universe level up. That might be what Tosun is doing.

Andrew Swan (Jan 30 2024 at 09:34):

If you want to do that kind of argument in the internal language of a locally cartesian closed category directly, you need the extra assumption that your category has enough universes. That's usually a safe assumption, in the sense that it holds in most natural examples of $\Pi W$-pretoposes, although a little inelegant, since universes aren't uniquely defined up to isomorphism by universal properties.

Madeleine Birchfield (Jan 30 2024 at 11:09):

But absent any universes, such as a $\Pi W$-pretopos with internal fullness but nothing else, this argument doesn't go through.

Madeleine Birchfield (Jan 30 2024 at 11:23):

Also, with enough universes, you might as well just use frames and locales directly (usually considered impredicative) and just recognize that the frames and locales lie in the next universe level.

Andrew Swan (Jan 30 2024 at 11:25):

It's hard to say whether universes are necessary without looking at the details of the proofs. If there's a proof in type theory that uses universes then sometimes it's very easy to remove them and make the argument work in an arbirtary lcc, sometimes it's possible but non trivial, like the derivation of dependent W-types from non-dependent W-types, and sometimes it's impossible, like the proof coproducts are disjoint. For proofs involving formal topologies I think it's worth checking to make sure they can be made to work without universes.

Andrew Swan (Jan 30 2024 at 11:25):

If fullness is referring to the fullness/subset collection axiom, then it's not clear how to even state it internally without either a universe or a class of small maps, like in algebraic set theory.
Edit: I suppose you can use stack semantics to state fullness, so that would avoid using universes.

Andrew Swan (Jan 30 2024 at 11:32):

Madeleine Birchfield said:

Also, with enough universes, you might as well just use frames and locales directly (usually considered impredicative) and just recognize that the frames and locales lie in the next universe level.

That's possible, but formal topologies can still be useful. In the paper by Gambino at https://doi.org/10.1016/j.apal.2005.05.021 the truth values in a Heyting valued model of set theory are elements of a frame, which can be a proper class, but to prove soundness it's important that the frame comes from a set presented formal topology.

Madeleine Birchfield (Jan 30 2024 at 11:48):

What happens if you replace the set of truth values $\Omega$ with a dominance $\Sigma \subseteq \Omega$ in the definition of cover or formal topology?

Madeleine Birchfield (Jan 30 2024 at 12:01):

Andrew Swan said:

If fullness is referring to the fullness/subset collection axiom, then it's not clear how to even state it internally without either a universe or a class of small maps, like in algebraic set theory.
Edit: I suppose you can use stack semantics to state fullness, so that would avoid using universes.

Speaking of the stack semantics, a function $P:A \to \Omega$ into the set of truth values is equivalently a set $P$ with an injection $P \to A$; internally in a category this is an object $P$ with a monomorphism $P \to A$. So I wonder if we could use the stack semantics to define the inductive covers without using universes.

Andrew Swan (Jan 30 2024 at 12:03):

Madeleine Birchfield said:

What happens if you replace the set of truth values $\Omega$ with a dominance $\Sigma \subseteq \Omega$ in the definition of cover or formal topology?

I guess that makes sense as a definition, but the question is how it would work with examples. E.g. the Heyting algebra of open sets of real numbers is a proper class in a predicative setting - you can deal with this by working with a set presentation of formal topology, but it's still useful to have some way of talking about arbitary open sets.

Andrew Swan (Jan 30 2024 at 12:05):

Madeleine Birchfield said:

Andrew Swan said:

If fullness is referring to the fullness/subset collection axiom, then it's not clear how to even state it internally without either a universe or a class of small maps, like in algebraic set theory.
Edit: I suppose you can use stack semantics to state fullness, so that would avoid using universes.

Speaking of the stack semantics, a function $P:A \to \Omega$ into the set of truth values is equivalently a set $P$ with an injection $P \to A$; internally in a category this is an object $P$ with a monomorphism $P \to A$. So I wonder if we could use the stack semantics to define the inductive covers without using universes.

Yes, that might work.