Strict Category Theory

[JacquesCarette]

Related to #35 .

So in branch Strict, I implemented a lot of Strict category theory, with a particular design in mind: That Category itself wouldn't be parametrized by an equality, but would use the surrounding propositional equality ≡ instead. Quite a lot of stuff can be defined. But eventually things "stop working". Here are some of them:

• Functor equality. Using ≡ doesn't quite work, as Functor contains functions, and we don't have extensionality. One can definitely define

    _≡F_ : ∀ {o ℓ} {o′ ℓ′} {C : Category o ℓ} {D : Category o′ ℓ′} → (F G : Functor C D) → Set (ℓ′ ⊔ ℓ ⊔ o ⊔ o′)

  (there are variations, the one in the code turns out to be sub-optimal). Of course, one problem with that definition is that it is exactly that: a definition. Which means that it isn't ≡ 'on the nose'. Now, it's quite close, and one would hope to be able to define an eliminator from that data into ≡. Alas, as far as I can tell, that needs axiom K to work.

• Things really start to break down in trying to provide examples / instances. Showing that (for instance) two Monoid Homomorphisms are ≡ is again really hard without extensionality and without proof irrelevance. In other words, one needs to assume that the carrier is a set (in the HoTT sense of the word). This isn't so weird for Monoid. But for Cats (the category of categories) things get worse, and brings us back to _≡F_: since Functors are not nicely 'equal', one needs to instead use (weak) Category that allows us to give a _≡_ parameter. Then things do work (but the proofs are painful).
• This of course infects other definitions, in particular 2-Category needs to use the weak definition of Enriched because the resulting Monoidal 2-Category Cats over which we enrich is weak.
• But things are worse still as the Functors Category can't really even be written down! It is supposed to be a strict category, but proving associativity (etc) requires equality of Natural Transformations, whose equality is even more difficult to write down properly (η is a function whose rhs is dependently typed).

In other words, if the meta-theory is intensional, using propositional equality as a stand-in for "equality" for Strict categories just doesn't work. This is where CT seems to be very sensitive to its meta-theory, and its usual meta-theory is still haunted by set-theoretic, extensional thinking.

[JacquesCarette]

I gave it another try. Much of which is now checked-in, so that there is a definition of 2-Category now. And it is indeed 'Strict', and some other stuff along with it.

But it eventually breaks down. Again, extensionality is an issue. For example, the category Functors with objects Functor and NaturalTransformation as morphism, cannot have ≡ as its object equality; well, it can, but nothing about it is provable. [Proof relevance would also be a problem, but extensionality hits first].

My thinking is that Strict category theory is a very Set-based phenomenon, where it makes sense to have a single, global equality relation, and where proofs are not first-class. As some of it does work, it is checked in. But I would not be heartbroken if that was reverted. There's also some incomplete code in the Strict2Cat branch, to show where things really hopelessly break down.

My conclusion is that in ITT/MLTT, 'Strict' categories must actually be "locally strict" in the sense that Obj must be a Setoid, in the same way that currently Hom is Setoid enriched. Of course, just like \o-resp-\~~ needs to be added for things to work, something similar would be needed too.

[sstucki]

So in branch Strict, I implemented a lot of Strict category theory, with a particular design in mind: That Category itself wouldn't be parametrized by an equality, but would use the surrounding propositional equality ≡ instead.

Could you elaborate a bit on that? It seems a strange thing to do in an intensional type theory, no? Since category theory traditionally assumes an "extensional" meta-logic, it would surprise me if one could express many interesting things using such a weak notion of equality. Doesn't one either have to go with Bishop's approach of using setoids, or go the HoTT route and assume additional axioms (e.g. univalence)?

My conclusion is that in ITT/MLTT, 'Strict' categories must actually be "locally strict" in the sense that Obj must be a Setoid, in the same way that currently Hom is Setoid enriched.

That seems reasonable to me. And for some constructions I believe it's actually necessary (see my comments in #41). Of course this will complicate definitions substantially.

But, I don't think that the difference of strict vs. weak category theory does/should ultimately come down to a particular choice of equality, or to object sets vs. object setoids. I think it comes down do the choice of coherence maps (unitors, associators, etc.)

The nLab page on bicatgories lists strict 2-categories as an example of bicategories:

Any strict 2-category is a bicategory in which the unitors and associator are identities.

Why not use this as a definition instead? Whatever the (local) notion of equality on morphisms is, it gives rise a notion of identity that can then be used to figure out the right "strictification", either directly or (where possible) by defining the weak structure first and then instantiating it to the strict case. Even though this sounds trivial, it is generally not: because we are in an intensional metatheory, identities (in the categorical sense) may have more structure than expected. E.g. in an extensional setting the domain and codomain of an identity are definitionally equal, but here they need not be. They need only be equal up to the identity the next level up.

For example, in #42, I propose a rework of functor equality that is based on this idea: strict functor equality is natural isomorphism where every component is an identity. But the domain and codomain of these identities need not agree definitionally.

Another example is the Gorthendieck construction. There's now an implementation for pseudofunctors, that involves a whole bunch of up-to-coherent-natural-iso constructions that would all have been identities in an extensional setting.

[JacquesCarette]

It's important to remember that I'm partly teaching myself category theory [the subtler points thereof] and constructive type theory while doing this. I'm an 'analyst' by training (i.e. the Pure Math version) and then evolved into a computer scientist. So I'm self-taught on almost all we're talking about here, which means that I have weird holes in my understanding.

In particular, I may well have made a really sub-optimal choice for Strict. If nothing else, under Strict, I should have assumed K. It would have worked quite a bit better. And indeed, choosing to use ≡ might simply have been a misguided choice. But I learned stuff by trying to push this through!

Yes, traditional CT does assume an extensional meta-logic. Here, in Agda, it is interesting to see exactly when that comes in. In the old library, some of that was swept under the carpet by using irrelevance, which is definitely where some things break down.

There might already be 2 HoTT-based libraries of CT (one in 'plain' Agda but assuming univalence, another in cubical Agda), but my understanding is that both are still fairly small. And certainly doing CT a la HoTT would be best done in cubical Agda. But that's a different library (no less interesting!).

Having said that, I definitely like the suggestion of starting from bicategory and understanding strictness as having certain data "be identities". One question though: how do we know that something 'is an identity' ? From the source code, it is straightforward. But internally in Agda, what is "is an identity" ?

[sstucki]

It's important to remember that I'm partly teaching myself category theory [the subtler points thereof] and constructive type theory while doing this. (...) And indeed, choosing to use ≡ might simply have been a misguided choice. But I learned stuff by trying to push this through!

Oh, well that sounds like an excellent project! I taught myself Agda by mechanizing type system proofs, and I learned a lot about both in the process. Ever since then, I feel I don't really understand a proof unless I mechanized it (irrespective of whether it's my own proof or someone else's). When it comes to category theory, I'm largely self-taught as well, so I'm grateful to you and @HuStmpHrrr that there's now an Agda library that allows me to explore CT in more detail and play around with them.

BTW, have you considered collecting your insights and experiences and publish them somewhere? I would be very interested to hear what you've learned. And in general, it would be nice to have some pedagogical resources for people with a programming/types background that are interested in category theory and vice-versa. And I don't mean people who want to use categories for programming — there's plenty of resources for that — I mean resources for understanding CT and TT foundations.

Yes, traditional CT does assume an extensional meta-logic. Here, in Agda, it is interesting to see exactly when that comes in. In the old library, some of that was swept under the carpet by using irrelevance, which is definitely where some things break down.

I totally agree. And one of the things I particularly like about this library is that it does not use "clever tricks" or fancy language features to cut corners. I'm really interested to see how much of "vanilla" category theory can actually be mechanized constructively, in "vanilla" MLTT, in practice.

One question though: how do we know that something 'is an identity' ? From the source code, it is straightforward. But internally in Agda, what is "is an identity" ?

I'm not sure I understand the question. What do you mean by 'internally in Agda'?

What I have in mind is that the precise meaning of 'identity' (and thus of 'strict') will depend on the context, i.e. the categories involved. Since categories already carry around a (local) notion of identity, that should be the thing that tells us what the right notion of strictness is.

I realize this is rather vague. I'm thinking of this as a guiding principle, rather than a general recipe. Maybe it would help to work out a few examples?

[JacquesCarette]

Yes, we're definitely planning to write up what we've learned. Outline is ready.

Re: identity - yes, I definitely think some examples would help. The notion of 'strict' in MLTT is still fuzzy for me. There are clearly some things that are strict already implemented; the accompanying functors have idf and (generally) refl or other 'free' proof obligations, or the accompanying natural transformations have id arrows uniformly. But that's kind of a meta-theoretic observation.

[JacquesCarette]

There's been a lot of discussion on this issue, but I'm still not entirely sure what to try next. There are intriguing ideas above, but rereading it all, I don't quite know what to try. I would still be curious to see how far one can push things through via using ≡ as the equality, but of course in a setting with K as well. But this may well be doomed - so if someone can enlighten me as to that, I would most appreciate it!

[sstucki]

First, a question. I'm still confused in what sense using one equality or the other determines whether a categorical structure is strict or weak (in the category-theoretical sense).

Concepts I would consider strict:

• the category Cat (as in Instance.StrictCats),
• enriched categories (e.g. Category and 2-Category in this library),
• functor equality (Functor.Equivalence in this library).

Concepts I would consider weak/non-strict:

• the category Ho(Cat) (as in Instance.Cats),
• bicategories and weakly enriched categories (e.g. Bicategory.Instance.Cats)
• natural isomorphism.

I fail to see how this relates to choosing ≡ as the equality on morphisms. With the exception of functor equality, none of these even involve ≡ in the current library. So what's the connection?

I would still be curious to see how far one can push things through via using ≡ as the equality, but of course in a setting with K as well. But this may well be doomed - so if someone can enlighten me as to that, I would most appreciate it!

I think problems would mostly crop up in instances and constructions. For example:

• working with quotients, e.g. proving Sets is (finitely) cocomplete/has equalizers/pushouts;
• working with structures that have "proof-irrelevant" parts and/or are equal up-to some (proof-irrelevant) equivalence, e.g. the category of binary relations (≡ is too strict an equality), spans, etc. — this is obviously related to the previous point;
• working with extensional equality, e.g. proving Sets is cartesian closed.

Though I have not checked any of these, so there might be something I'm missing.

[sstucki]

To clarify, my question/confusion is ultimately about the title of this issue: "Strict Category Theory". Maybe you just mean something different by "strict".

If that's the case, then maybe I should open a separate issue that is about how to organize strict vs. weak constructions (in the categeorical sense), which is what I thought this issue was about.

[JacquesCarette]

More relevant discussion at #44 and #58.

[JacquesCarette]

So I think it might be time to revisit this. What is quite clear is that the word 'strict' is used for a lot of different things in CT, and should not all be lumped together. So this 'issue' really ought to be several issues, with this one closed as obsolete/confused. I then think every one of the separate issues can be tackled separately.

The reason I'm not just doing that myself, is that I need some help to figure out what are the separate issues involved!

[JacquesCarette]

And now I am closing it, but I left a link on the projects page.