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: -1-categories, constructively

Jacques Carette (Jan 01 2021 at 19:15):

A (-1)-category is classically the set of truth values. One can read quite a bit more about them in the arxiv'ed paper by @John Baez and @Mike Shulman Lectures on n-Categories and Cohomology.

But I am here interested in the constructive version of -1-categories. Given excluded-middle, it is indeed easy to prove that the category of -1-categories indeed only has 2 inhabitants up to equivalence, and is equivalent to a set. One can start from -2-categories being 1-categories that have (inhabited, contractible) objects and contractible homs (for example), and this 'works' too. One can then define a monoidal structure on that. And then define -1-categories to be categories enriched over those -- everything works out nicely: basic definition of -2-category, and the equivalence to One, and then -1 category.

However, as far as I can tell, to show that -1-categories are only the truth values seems to really require excluded-middle. In fact, I strongly suspect that it is equivalent to it. Roughly the idea is simple: Suppose that the category of -1-categories is indeed equivalent to the category with only 2 inhabitants (and we have an explicit equivalence witnessing this fact).
Take any type, build 'the' indiscrete category over it, which can be shown to be a -1-category and then look to see what it maps to, true or false? That tells you whether it's inhabited or not, which gives you that inhabitation is decidable (i.e. a very strong excluded middle - way too strong).

So that sketch is wrong somewhere, in that it likely uses excluded middle itself. It's ok to ask if something is 'true' or 'false', as that is indeed decidable, but that's not quite what is in the sketch, is it? What's there is 'is it the true or false -1-category', which isn't necessarily decidable.

My intuition is still that, constructively, -1-categories can't be shown to be equivalent to merely the 2 classical truth values. And assuming that it can, implies some classical axiom. But I'm currently stuck on the details. Any help would be appreciated.

Dan Doel (Jan 01 2021 at 19:24):

Constructively, it's not the case that 'every truth value is either false or true'. So, if by "the truth values" you mean "false and true," that's using classical terminology.

Dan Doel (Jan 01 2021 at 19:40):

E.G. in HoTT, the truth values are what people call propositions, specified by $\mathsf{isProp}(A) = Π_{x,y:A}x \equiv y$, but it is erroneous to think that $\mathsf{isProp}(A) → (A \equiv ⊤) + (A \equiv ⊥)$

Dan Doel (Jan 01 2021 at 19:42):

That would be excluded middle.

Reid Barton (Jan 01 2021 at 19:43):

Well, it's not "erroneous", you're just working in a logic too feeble to prove it. :upside_down:

Dan Doel (Jan 01 2021 at 19:53):

That would be an erroneous answer to the question.

Jacques Carette (Jan 01 2021 at 20:25):

Right. So one of the things I'm trying to establish is exactly that: assuming that there are exactly 2 -1-categories is equivalent to excluded middle. My proof doodles all seemed tentalizingly close, but never quite 'there'.

The other thing I'm trying to establish is a charaterization (in MLTT) of what -1-categories 'are'. Perhaps they are exactly the values that $\mathsf{isProp}$ can take?

Dan Doel (Jan 01 2021 at 20:35):

I think it would probably coincide, since it's trivializing enough stuff for there to be no difference between the category and groupoid versions. But I kind of forget the details.

vikraman (Jan 02 2021 at 19:04):

Consider the -1-category whose set of objects is $\{x \in 1\;|\;\phi\}$ and identity morphisms. If there are only two -1-categories 0 and 1, this implies $\phi \vee \neg\phi$.

Jacques Carette (Jan 03 2021 at 14:43):

Hi @vikraman . That's exactly what I've been trying to convince Agda is true... with no success. It is entirely possible that I'm not phrasing the 'question' quite correctly (in Agda) and that's the real source of the problem. And of course "only two" means "up to categorical equivalence" (which should be fine), but does make the reasoning a tiny bit trickier.