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: reading & references

Topic: Statement from Propositional Resizing

Noah Chrein (Nov 21 2024 at 16:56):

Hello! I am looking for a reference to read a bit more about the following statement from the propositional resizing nlab page which states:

it is still possible to define a well-pointed cartesian closed lextensive coherent category object with a natural numbers object inside of any well-pointed cartesian closed lextensive coherent category with a natural numbers object.

If someone could point me in the right direction that would be well appreciated!

I am investigating how one uses these as universe hierarchies, for the sake of generalization.

Madeleine Birchfield (Nov 21 2024 at 17:53):

That paragraph seems to be about about defining models of the category of sets inside of a weak foundational set theory, cloaked in the language of category theory.

Madeleine Birchfield (Nov 21 2024 at 17:57):

well-pointed = axiom of extensionality / function extensionality
coherent = products + singletons + preimages / solution sets + image factorisation + most logical operations / quantifiers
cartesian closed = function sets + implication/universal quantification
lextensive = empty set + disjoint unions
natural numbers object = natural numbers

Madeleine Birchfield (Nov 21 2024 at 18:02):

Also I don't think the paragraph is true because of size issues.

Noah Chrein (Nov 21 2024 at 18:29):

Yes! It is exactly about that, but I would like a reference to explore the exact mechanisms by which this works/why all these assumptions are needed

not true because of size issues

I'm actually explicitly not worried about this, I know it will come back to haunt me but I am more interested in the functorial semantics of structural specification (i.e. internal ____ ), and how one functorially encodes structure that can functorially encode structure that can functorially encode structure...etc

Noah Chrein (Nov 21 2024 at 18:59):

^ and if this kind of functorial specification "chain" can be used to replace universe hierarchies. The same page states these lex__categories can be viewed as universes.

Madeleine Birchfield (Nov 22 2024 at 22:34):

It's the same process that set theorists do when they talk about constructing models of ZFC inside of a model of ZFC + an inaccessible cardinal, only here it's using ETCS-like categorical set theories with an "inaccessible set" to construct a model of said categorical set theory. You treat the outer category as your foundations of mathematics and then construct ΠW-pretoposes in the category. (I'm not sure why the author of the paragraph in the article rejects quotients, usually people talk about pretoposes rather than lextensive coherent categories)

Madeleine Birchfield (Nov 22 2024 at 22:52):

Noah Chrein said:

not true because of size issues

I'm actually explicitly not worried about this, I know it will come back to haunt me

Noah Chrein said:

I am investigating how one uses these as universe hierarchies, for the sake of generalization.

Universe hierarchies are directly related to size issues; if the universes are closed under finite limits and finite colimits they are related to regular cardinals; if additionally they are closed under exponentials or power objects, they are related to inaccessible cardinals; and if they contain another universe inside them, then they are related to the next regular or inaccessible cardinal.

Madeleine Birchfield (Nov 22 2024 at 22:59):

Noah Chrein said:

I am more interested in the functorial semantics of structural specification (i.e. internal ____ ), and how one functorially encodes structure that can functorially encode structure that can functorially encode structure...etc

You would probably be looking for the analogue for whatever category is being talked about in that paragraph of the concept of a fully faithful [[logical functor]] between elementary toposes or a fully faithful [[cartesian closed functor]] between cartesian closed categories. Some fully faithful functor which preserves all the relevant structure in the categories.

I don't personally know of any sources which explicitly talk about fully faithful structure preserving functors between ΠW-pretoposes or ΠW-lextensive coherent categories.

Madeleine Birchfield (Nov 22 2024 at 23:01):

Noah Chrein said:

^ and if this kind of functorial specification "chain" can be used to replace universe hierarchies. The same page states these lex__categories can be viewed as universes.

The chain of fully faithful functors wouldn't be used to replace universe hierarchies. They would be used to define universe hierarchies.

Madeleine Birchfield (Nov 22 2024 at 23:12):

In any formulation of dependent type theory where the universe hierarchy is not cumulative, universe hierarchies are defined as having a lifting operations called between universe types. The lifting operations play the role for universe types in dependent type theory that fully faithful functors play for the categories in the categorical set theory.

Noah Chrein (Nov 27 2024 at 17:04):

Thank you @Madeleine Birchfield for your responses. I am not as interested in modeling set as I am in the functorial semantics of structural specification.

For the future I will call well-pointed cartesian closed lextensive coherent category with a natural numbers object a "Lex" category for short.

By functorial semantics I mean it in the sense of doctrines: encoding axioms of an $X$ -structure as a structured category in a doctrine $\underline{X}:\mathbb D$ and realizing $X$ -objects as functors out of $\underline{X}$ , i.e. $\mathbb D(\underline{X}, C)$ . For example monoids in set are monoidal functors out of $\Delta_+: Cat_\otimes$ so that $Mon \cong \mathbb Cat_\otimes(\Delta_+,\text{Set})$ .
I imaging then there is some "doctrine" $Lex$ with an object $\underline{lex}:Lex$ so that for $L:\text{Lex}$

a well-pointed cartesian closed lextensive coherent category object with a natural numbers object inside of any well-pointed cartesian closed lextensive coherent category with a natural numbers object.

is a structure preserving functor $\underline{lex} \to L \;\;\; :\text{Lex}$

but the paragraph goes further to say:

These objects are called universes or Grothendieck universes

which makes me think that one can see universe hiearchies as follows:

start with the category (?) of Lex categories $Lex$
consider a lex category $\underline{lex}:Lex$ that "encodes the axioms of lex categories"
define $Lex_0:= Lex(\underline{lex}, S)$ , the Lex-category objects in some lex category $S:Lex$
Now we have something like $Lex_0:S$ , to mean " $Lex_0$ is a lex category object in $S$ ".

Can we continue this process $Lex_{n+1}:=Lex(lex, Lex_n)$ to produce a chain of universes like:
$Lex_n:Lex_{n-1}:...:Lex_2:Lex_1:Lex_0:Lex$

I know for certain I am way off the mark with this idea in some way, but the way I have been thinking of universes is as chains

A:Theory:2-Theory:...

where the "2-theory" endows the "theory" with the structure necessary to specify the structure of A. In this case, a Lex category endows lex categories with the ability to specify the structure of lex categories...