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: Defining "finite category"

Jacques Carette (May 14 2020 at 18:49):

[Caveat: this is a basic question, not a beginner question]

How do I define "finite category" if I am in a

1. constructive context (so no excluded middle, and no choice)
2. I do not wish to refer to equality of objects (really, not at all) ?
   [A definition in type theory, such as Martin-Loef Type Theory, would be perfect.]

For example, how do you define FinSet (the category of finite sets and functions) in such a setting? Or Bij [finite sets and bijections]?

You can't assume that you have an iso $X \simeq \Sigma\ \mathbb{N}\ \mathsf{Fin}$ for example, as that would let you transport the decidable equality of the rhs onto the lhs. Worse, you even get an ordering on $X$! And since we're not in HoTT, no, propositional truncation is not available either.

Definitions involving language like "equivalent to a finite skeletal category" are not better (as the nLab page explains).

Jem (May 14 2020 at 19:44):

Which nLab page are you referring to - I can't see it on the finite category page?

Jacques Carette (May 14 2020 at 19:45):

I'm referring to the skeleton page, sorry, I wasn't precise enough.

Jem (May 14 2020 at 19:56):

Would "category $C$ with finite hom-sets and with essentially surjective on objects functor from a finite discrete category (i.e. from a finite set)" work?
Of course this has extra data (the e.s.o functor), and your type of objects isn't "actually" finite - is that close enough to what you want?

Jacques Carette (May 14 2020 at 20:16):

Essentially surjective on objects is either too weak (because it builds in 'merely exists' which is propositional truncation) or too strong (if you use $\Sigma$) as you can recover too much from that, as that becomes a choice function.

Jacques Carette (May 14 2020 at 20:34):

Coquand and Spiwack's Constructively Finite? is a good entry point into the intricacies of "finite" constructively. A nice follow-up is Firsov, Uustalu and Veltri's Variations on Noetherianness in MSFP 2016 that continues to weave that tale. Figure 1 on the last page is a nice visual of the "design space".

Reid Barton (May 14 2020 at 20:37):

I don't understand the question. FinSet is not a finite category. What do you want to define exactly?

Reid Barton (May 14 2020 at 20:38):

Is the question how to define FinSet in a constructive setting?

Jacques Carette (May 14 2020 at 20:39):

Sorry, yes, of course FinSet isn't finite. Yes, I'm interested in defining FinSet in a constructive setting.

Reid Barton (May 14 2020 at 20:47):

Well, as far as I can see, the question just seems to reduce to understanding what you mean by "finite set" in the first place, and presumably the meaning will depend on the desired application.

Reid Barton (May 14 2020 at 20:48):

If you have a notion of "finite set" presumably there is a way to get the underlying type out, and then the morphisms of the category would just be all morphisms (or all isomorphisms) between the underlying types.

Jacques Carette (May 14 2020 at 20:54):

Let me start with the context / desired application: a formalization of "wild" category theory (i.e. Setoid-Enriched Categories with Types as objects with no equality) in Agda, using 'pure' Martin-Loef Type Theory, without the K axiom.

On top of that, I'm currently working on formalizing Species, as functors from core(FinSet) into Set. Well, core(FinType) into Setoids to be precise. [All of this work is publicly visible in the github repo for agda-categories.]

But I'm not satisfied with my definition of FinSet. And I'm not happy with my co-author's definition of Finite Category either (as being any category that is adjoint equivalent to a 'shape' category built on Fin for objects and finitely enumerated Hom sets).

Reid Barton (May 14 2020 at 20:59):

Well, of course you cannot mechanically take a concept that lives originally in classical mathematics and make sense of it in a constructive setting, because this process cannot preserve equivalence of concepts.

Reid Barton (May 14 2020 at 21:00):

In other words, you face a creative problem, not a technical one

Reid Barton (May 14 2020 at 21:00):

which may have more (or fewer) than one solution

Jacques Carette (May 14 2020 at 21:00):

Right!

Reid Barton (May 14 2020 at 21:01):

but the solution to this problem is presumably going to be intimately related to details of the theory of species

Jacques Carette (May 14 2020 at 21:01):

I've kind of exhausted my creative juices on this one, so I figured I would ask the experts, who might have already thought about it, and come up with some reasonable solutions.

Jacques Carette (May 14 2020 at 21:02):

I am trying to do two things (and willing to have 2 "solutions"): a generic CT library, and a particular implementation of Species.

Jacques Carette (May 14 2020 at 21:04):

For Species, I am exploring the nature of the definitions, to try to see the necessary assumptions for each construction. [Yes, I know about 'Generalized Species'].

Jacques Carette (May 14 2020 at 21:17):

For example, the One species is usually defined on objects via "if the input set is of size 1, then that set as a singleton, else empty" (which can be made fully precise). But a much more generalizable definition is "the hom Setoid from 'the' terminal groupoid to the given groupoid". 63 lines of Agda versus 2 lines.

So the latter version captures the choice being made much more nicely. And clearly generalizes a lot more.

Jacques Carette (May 14 2020 at 21:18):

Hmm, I should probably link to the nice html version rather than directly to the sources.

John Baez (May 14 2020 at 22:04):

I've nothing interesting to compute, but I'm glad you're trying to code up species!

For example, the One species is usually defined on objects via "if the input set is of size 1, then that set as a singleton, else empty" (which can be made fully precise). But a much more generalizable definition is "the hom Setoid from 'the' terminal groupoid to the given groupoid".

Why does the latter definition give something empty if you're working with sets and "the given groupoid" is a set with two elements? I'd think it gives a 2-element set.

Jacques Carette (May 14 2020 at 22:16):

Sorry: Hom over Groupoid. i.e. $Hom[ 𝔹 ][ ⊤-FinSetoid , - ]$. ⊤-FinSetoid is here promoted to a Groupoid because Species is defined as
Functors (Core (FinSetoids o ℓ)) (Setoids o′ ℓ′)
(the category of functors from the Core of FinSetoids to Setoids). Where the above is the exact line of Agda defining that.

Reid Barton (May 14 2020 at 22:18):

By the way, why not just work in a setting with quotients? Isn't all this Setoid stuff terribly tedious?

Jacques Carette (May 14 2020 at 22:19):

Turns out that working with Setoids, at least for Category Theory, is not tedious at all. That was a big, but welcome, surprise.

Jacques Carette (May 14 2020 at 22:20):

It is akin to working in 1.5-Category, i.e. some of the stuff from 2-Categories peek through early. But that's it. And hopefully no one here considers 2-Categories 'tedious' ;)

Reid Barton (May 14 2020 at 22:28):

I will choose to remain skeptical.

Reid Barton (May 14 2020 at 22:28):

Also, 2-categories are in fact quite tedious. :upside_down:

Reid Barton (May 14 2020 at 22:30):

For instance, compare the definition of a symmetric monoidal 2-category to that of an ordinary symmetric monoidal category. "No worse than blowing up the dimension of everything by one" isn't much of an endorsement.

James Wood (May 14 2020 at 22:35):

When your only source of equalities is axioms, and your only use of equalities is to prove more axioms, I can believe that there'd be little benefit in using identity types.

James Wood (May 14 2020 at 22:37):

Data-heavy work (which category theory is almost explicitly not) seems to be where you get wanting identity types.

John Baez (May 14 2020 at 22:42):

But category theory intrinsically wants to become n-category theory or at least $(\infty,1)$-category theory.

Reid Barton (May 14 2020 at 22:42):

Well, identity types do have this handy property that $x = y \implies f(x) = f(y)$ for any $f$.

Reid Barton (May 14 2020 at 22:42):

But, different strokes for different folks I guess.

Reid Barton (May 14 2020 at 22:51):

By the way, @Jacques Carette, did you say you had a formalization of multicategories somewhere? I'd be curious to take a loook.

Jacques Carette (May 14 2020 at 23:27):

@Reid Barton Sort of. Fin-based Multicategories completely stumped me. There are many (implicit) uses of a lot of theorems of arithmetic buried in the definitions that need to be made explicit to please any ITP. However, if you go to "Indexed Multicategories" instead, then it's relatively straightforward. The pretty version is at https://agda.github.io/agda-categories/Categories.Multi.Category.Indexed.html . The key part is that the axioms rely on lower-level axioms on the index sets (the multiplicative monoid structure of Type). The tricky definition is composition. Once that's straight, the rest follows.

Morgan Rogers (he/him) (May 15 2020 at 12:01):

Relevant topics from the topos theory stream, finite objects and predicative finiteness.
I don't know enough about the setoid setting to meaningfully contribute without making a blunder, but perhaps seeing the different definitions of finite objects in the topos context, and how they can be defined, might help?
Something that scared me when I saw someone working with groupoids for the first time is that without equality you won't be able to distinguish between finite categories and "essentially finite" categories: those which are merely equivalent, in whatever sense you have available, to finite ones. Of course, this isn't really a problem, since the notion of equivalence means that even if they externally look different (ie you are able to construct a type which is infinite in some sense but equivalent in your type theory to a finite thing), they'll internally be functionally indistinguishable. :+1:

Jacques Carette (May 15 2020 at 12:03):

Thanks for the pointers @Morgan Rogers, reading now . Note that I consider "finite up to categorical equivalence" to be a feature, not a bug.

Morgan Rogers (he/him) (May 15 2020 at 12:05):

The speaker defining finiteness in that context convinced me of the same. I wish I could remember who was speaking and where that talk was, it would probably be a lot more helpful. I suspect it might have been Benedict Ahrens, but I could be wrong.

Reid Barton (May 15 2020 at 12:16):

It may or may not be worth mentioning that there are multiple notions of equivalence and even functor in a constructive setting (or even just without choice): https://ncatlab.org/nlab/show/anafunctor

Reid Barton (May 15 2020 at 12:22):

Though maybe this other notion doesn't really exist if you don't even have a way to express a non-split surjection?

Jacques Carette (May 15 2020 at 12:22):

It does bear repeating. I've been meaning to write about that - I think the traditional definitions here are too overshadowed with what happens in 0-category theory, where g can be fully reconstructed. I see that as an accident because things are "too small". The anafunctor way out is to build-in to f the crucial data needed to reconstruct g !

Reid Barton (May 15 2020 at 12:24):

Oh, I guess in your language a non-split surjection is a map of setoids with an inverse that does not respect the equivalence relation.

Jacques Carette (May 15 2020 at 12:25):

Rereading https://ncatlab.org/nlab/show/finite+set, I think that a generalization of Dedekind-finite might be what I'm after.

Jacques Carette (May 15 2020 at 12:26):

@Reid Barton right. We never look at those. Respecting the equivalence is built right in (but requires proof).

Jacques Carette (May 15 2020 at 12:38):

Would it be reasonable to call a Category C "Dedekind finite" if any faithful endofunctor $F : X \rightarrow X$ must be an equivalence? (Probably want to go for 'part of an adjoint equivalence')