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: theory: category theory

Topic: Stuff about n-Categories

Reuben Stern (they/them) (Apr 16 2020 at 14:51):

Whenever I say "$n$-category" I'm really thinking of $(\infty, n)$-categories, so I apologize if the things I say don't strictly (pun intended) make sense in the world of ordinary n-categories. Let me start in the case $n = 2$ for concreteness. There are a few different notions of co/limits: 2-co/limits over 2-categories (or 1-categories considered as 2-categories with no non-invertible 2-cells), lax co/limits over 1-categories, and general weighted co/limits, of which the first two are examples.

It seems to me that lax co/limits and 2-co/limits are "orthogonal", in the same way that finite and filtered colimits are. A 1-category has all colimits if it has finite colimits and filtered colimits. Is a statement of the following form true?

Desideratum: A 2-category has all weighted colimits if it has all lax colimits and all 2-colimits.

Much more generally, whenever $m < n$, we can think about "$m$-lax co/limits" over $m$-categories in $n$-categories; then maybe a statement of the following form is true?

Desideratum: An $n$-category has all weighted colimits if it has all $m$-lax colimits for $1 \leq m < n$ and all $n$-colimits.

Reid Barton (Apr 16 2020 at 15:09):

I'm not very good at this lax stuff. If $C$ is a 1-category and $X$ is an object of a 2-category, is the tensor $C \otimes X$ the same as the lax colimit of the constant diagram on $C$ (or maybe $C^\mathrm{op}$) with value $X$ (when they exist)?

Reid Barton (Apr 16 2020 at 15:13):

I think it's true for lax limits in Cat, so I guess the answer is yes by representability?

Reuben Stern (they/them) (Apr 16 2020 at 15:18):

I think you're right. If $F: \mathcal{C} \to {\mathsf {Cat}}$ is constant at $\mathcal{X}$, is the unstraightening $\mathcal{E} \to \mathcal{C}$ the tensor $\mathcal{C} \otimes \mathcal{X}$?

Reid Barton (Apr 16 2020 at 15:22):

In Cat the tensor product is the cartesian product, so I'm pretty sure the answer is yes.

Reuben Stern (they/them) (Apr 16 2020 at 15:23):

Then yeah, your claim is right (by Gepner--Haugseng--Nikolaus, but maybe it's easier)

Reid Barton (Apr 16 2020 at 15:29):

In that case I would guess that you can express weighted colimits in terms of ordinary/conical ones together with tensors, but my mind has blocked out whatever little I used to know about this.

Reuben Stern (they/them) (Apr 16 2020 at 15:51):

You're absolutely right! Thanks.

Mike Shulman (Apr 16 2020 at 15:53):

Reid Barton said:

you can express weighted colimits in terms of ordinary/conical ones together with tensors

This is a standard fact in enriched category theory (it must be in Kelly's book), which carries over to higher categories. However, it's worth noting that a particular weighted colimit in a particular category can exist even though the copowers (nee tensors) and conical colimits in terms of which it could be constructed don't individually exist.

Reuben Stern (they/them) (Apr 16 2020 at 15:54):

Mike Shulman said:

Reid Barton said:

you can express weighted colimits in terms of ordinary/conical ones together with tensors

This is a standard fact in enriched category theory (it must be in Kelly's book), which carries over to higher categories. However, it's worth noting that a particular weighted colimit in a particular category can exist even though the copowers (nee tensors) and conical colimits in terms of which it could be constructed don't individually exist.

Nice, thanks.

Henry Story (Apr 16 2020 at 16:50):

Can one dualise HoTT the way Constructive Logics have been dualisted into co-constructive logics (and type theories)? Would that give us a falsificationist Homotopy Type Theory, more apt for material reasoning? Just wondering...

sarahzrf (Apr 16 2020 at 17:25):

well, the standard semantics for cubical type theory are in a presheaf category, and im told that those always have bi-heyting structure (at least in a classical metatheory? i should work out if it's true in a constructive metatheory...)

sarahzrf (Apr 16 2020 at 17:25):

no idea whether there's a sensible way to reflect it into the syntax :thinking:

sarahzrf (Apr 16 2020 at 17:26):

and there are a bunch of restrictions on which presheaves are sensible to use as types, so actually i guess maybe it's not really "in a presheaf category"... hmmmm....

Mike Shulman (Apr 16 2020 at 17:54):

What do you mean by "material reasoning"?

Henry Story (Apr 16 2020 at 18:19):

"Material Reasoning" is a term I have found in Immanent Reasoning or Equality in Action, a book that gives a Dialogical explanation of Constructive Type Theory. The two last chapters speak about Material Dialogues, as opposed to Formal Dialogues. Formal Dialogues are what mathematics and logic tend to do more. You build a structure which is a proof. Material reasoning concern empirical examples I think, where Popper argued one can only falsify.

Henry Story (Apr 16 2020 at 18:25):

Actually that book gives a dialogical view of CTT with dependent types. It refers to the book by Trafford Meaning in Dialogue which looks at co-intutionistic logic, and argues that is what is needed for explaining dialogue, as well as making some arguments in terms of Category Theory (regarding co-exponentials). One sees the same type of inversions in "Immanent Reasoning..."s formal dialogues as Trafford argues for.
If there is a dual to HoTT, then that could perhaps be used to extend the dialogical explanation of CTT to HoTT.

Mike Shulman (Apr 16 2020 at 19:01):

I don't know of any useful way to dualize a dependent type theory, so I'd be interested to hear more. What I do know how to do is incorporate both proofs and refutations in a single affine logic via a Chu construction; that can certainly be done proof-relevantly (although there's only one remark about that possibility in the paper) but as far as I know only at the "top level" rather than allowing anything else to depend on it.

Mike Shulman (Apr 16 2020 at 19:01):

I do recall hearing from Favonia about some recent work in game semantics for dependent type theory, but I don't know anything about it.

Henry Story (Apr 17 2020 at 02:03):

The dual construction starts with selecting the subobject classifier $false: 1 \to \Omega$ of a Topos, as the subobject classifier for creating the dual topos, from which the dual-heyting structure arises. Perhaps something similar can be also done in an (infinity,1)-topos?
The Category Theoretic work seems to come from here Complement-Topoi and Dual Intuitionistic Logic

John Baez (Apr 18 2020 at 03:06):

Henry Story said:

The dual construction starts with selecting the subobject classifier $\mathrm{false}: 1 \to \Omega$ of a Topos, as the subobject classifier...

As I've explained before, you don't get to "select" the subobject classifier of a category: it either has one or it doesn't. And if you have a topos, $\mathrm{false}: 1 \to \Omega$ is not a subobject classifier.

You may be wanting to invent a concept of non-subobject classifier, or subobject "unclassifier".

Henry Story (Apr 18 2020 at 13:47):

John Baez said:

Henry Story said:

The dual construction starts with selecting the subobject classifier $\mathrm{false}: 1 \to \Omega$ of a Topos, as the subobject classifier...

As I've explained before, you don't get to "select" the subobject classifier of a category: it either has one or it doesn't. And if you have a topos, $\mathrm{false}: 1 \to \Omega$ is not a subobject classifier.

You may be wanting to invent a concept of non-subobject classifier, or subobject "unclassifier".

Yes, one has to be careful to get the naming right. Luis Estrada-Gonzalez in The Evil Twin: The Basics of Complement-Toposes looks at this problem in detail. There a dual-classifier appears, as well as anti-extensions, anti-comprehension axiom, dual characteristic morphism...
He develops the theory carefully and looks at the philosophical implications too (mentioning Hegel, Lawvere, ...)

Henry Story (Apr 18 2020 at 20:27):

At the end of the paper The Evil Twin: The Basics of Complement Toposes Estrada Gonzalez points out that the difference between Toposes and complement Toposes is not structural. It has to do with our naming ("Skolemization") of certain functions as true and false.

The mainstream topos-theorist can correctly insist on the categorial indistinguishableness between standard toposes and complement-toposes, but this amounts rather to a proof that both kinds of toposes equally deserve the name “topos,” since for all mathematical purposes they have the same constituents independently of Skolemization for the morphisms whose codomain is 􏰆. However, the internal logic induced is in fact different in each case, true, not by differences in the categorial structure, but in the way that categorial structure is described.
Although it sounds repetitive, it must be emphasized that the claim is not that complement-toposes are categorically different from toposes, nor to say that standard connectives acquire further categorial properties qua morphisms after the being renamed, but rather to stress the fact that the same categorial stuff, which is essentially equational with variables, can be described in at least two different ways.

Henry Story (Apr 18 2020 at 20:32):

This duality of trying to verifiy, construct or prove one one hand and disprove, falsify (deconstruct?) on the other does work very nicely for the dialogical view of logic.

Henry Story (Apr 19 2020 at 07:28):

To bring it back to this thread, in his introduction Estrada-Gonzalez writes about the limitation of his paper

Perhaps, the most important of them is that, although the new notions and constructions
introduced here do apply to first- or higher-order topos logic, for simplicity most
of my examples use only zero-order topos logic, so the reader will have to figure
out the higher-order cases.

So it looks like it should be quite possible to apply this to find a complement-HoTT, based I guess on inequalities?

Mike Shulman (Apr 19 2020 at 09:53):

I don't think "higher-order topos logic" refers to "higher toposes", but to aspects of the internal logic of 1-toposes that use the power objects and exponentials.

Henry Story (Apr 19 2020 at 10:35):

Thanks @Mike Shulman . That is beyond my abilities to judge, but it's getting me very interested in the area. I have a little Twitter thread on the topic https://twitter.com/bblfish/status/1251808172546949120

The intuition on complement Topoï comes from Topology. Constructive Logics work in Open Sets, inconsistent-tolerant Logics in closed sets (CSL). Is that because CSL include the border? Refutation logic aiming to disprove would be the one that sets the borders? https://twitter.com/bblfish/status/1251808172546949120/photo/1

- The 🐟‍‍ BabelFish (@bblfish)

Mike Shulman (Apr 19 2020 at 11:16):

For instance, the higher-topos/HoTT analogue of a subobject classifier $1\to \Omega$ starts with $\mathrm{Set}_* \to \mathrm{Set}$, the projection from the groupoid of pointed sets to the groupoid of sets. Unlike the inclusion of "true" into truth values (it's kind of just an accident that there is exactly one "pointed truth value") there is no obvious "complementary inclusion of false".

Henry Story (Apr 19 2020 at 17:07):

Perhaps by looking at Abramsky's 2015 article Games for Dependent Types one may find a way to understand how to think of a complement Topos for HoTT.
My thought is as follows: Trafford in Meaning and Dialogue uses the dual nature of a Topos to argue that it the co-Heyting algebra gives the logic of an Opponent. Immanent Reasoning or Equality in Action also gives a dialogical explanation of CTT with dependent types, and is quite easy to read. It does not mention complement Topoï, but the same patterns appear there when the Opponent plays. Abramsky does think his work is applicable to HoTT though, and that it can solve some outstanding problems. I did not understand the details when I read it a year ago. I am very slowly working my way toward it.