Challenge: prove that the Discrete functor is the (cartesian) left-adjoint of the forgetful functor from Cats to Sets

[sstucki]

Categories currently don't carry an explicit notion of equality on objects. This seems to be a "standard" way to mechanize categories constructively (as far as I'm aware), it is in line with the principle of equivalence, and it also simplifies the definition of Category greatly.

However, I'm worried that some rather elementary category theory silently assumes that objects really do have an equality (despite all the talk about this being evil). For example, one may define things like the hom-functor Hom : Cᵒᵖ × C → Sets from some category C to the category of sets. But in a constructive setting, we surely want to remember the notion of equality on morphisms in C so it's more accurate to type this as Hom : Cᵒᵖ × C → Setoids. (And this is indeed what seems to be implemented in Categories.Functor.Hom).

Another example is the adjunction between the forgetful functor from Cats to Sets and the Discrete functor in the opposite direction. In text-book category theory, both Cats and Sets are CCCs, so this adjunction should consist of a pair of cartesian functors. Following a short discussion with @JacquesCarette on Twitter, I have tried to mechanize this IMO very elementary result, but have failed so far. Here's a summary of what I've tried so far:

• Show that Sets is cartesian closed — this fails because it seems to require function extensionality (at least as Sets is currently defined).
• Use Setoids, which is a CCC, instead of Sets. Now we need to pick a notion of equality on objects as we go from Cats to Setoids.
  • Use isomorphism (don't be evil) — this isn't truly forgetful but results in a truncation because we are effectively quotienting objects by isomorphism. There is no left-adjoint because truncation forgets equality proofs of morphisms, which are required to define the counit.
  • Use propositional equality (be truly forgetful) — there is again no left-adjoint because the unit would have to (propositionally) identify setoid elements that are only equivalent.

There might be other options, but ultimately I think that if one wanted to mechanize a "classic" text-book on category theory, one would be forced to use a more "evil" notion of constructive categories, such as Palmgren's H-categories. I don't think that's too bad though. I see no reason that the two notions of categories could coexist in the same library, in principle.

[JacquesCarette]

Same comment as on #40: soon. And this is very interesting!

[HuStmpHrrr]

I feel terrible these couple days. my school decides to exhaust me before letting me go. I think I will have to rest before looking deeper.

indeed, Sets being a CCC relies on functional extensionality, but Setoids doesn't seem to suffer this problem. Cats being a CCC requires all three indexing levels are identical, which is quite unsatisfactory. I believe @JacquesCarette and I had such discussion before.

I suppose the distinction comes from the fact that the category theory built here is somewhat a "weaker" notion than in usual sense. the usual category theory considers hom to have merely a set structure, so it's typically algebraic, while in this library, with proof relevance hom setoids are really arbitrarily rich.

[JacquesCarette]

So I've gone down the same rabbit hole that @sstucki did. And, unsurprisingly, rediscovered the same things. To be precise, the failure in the definition of the counit when using isomorphisms is that Functor underlying the NaturalTransformation cannot respect equality (i.e. there's no proof of F-resp-≈) because the data needed for that is forgotten.

I wonder if rather than using a hard-truncated equivalence, one were to use something contractible instead? Some kind of 'local' K axiom.

Is the conclusion to be drawn here that, constructively, Discrete is not a particularly useful notion, as it is dependent, in a fragile way, on the underlying equality being extensional? Or maybe just that it must satisfy UIP? In other words, instead of keeping all of _≅_ around, maybe if we were more forgetful still, and imposed that all of them are equivalent to each other.

[JacquesCarette]

Progress, of sorts. The Discrete Category page on nLab is quite specific:

A category is discrete if it is both a groupoid and a preorder. That is, every morphism should be invertible, any two parallel morphisms should be equal.

This was not really how things had been done. So now there is a proper Discrete predicate for this. The 'strict' case continues to go through just fine, but the Setoid version still does not, even though it's much closer. The problem still is that the morphism equality is uninformative. I think what's needed is a notion of 'CoherentSetoid' with a morphism equality notion that automatically makes it into a Groupoid. The preorder condition should then be enough, I think.

[sstucki]

Interesting! I had kinda given up on there being any progress on this issue, TBH. 😄

Also, nice to know the nLab-version of discrete category, I wasn't aware of that one. Though I'm pretty sure I've checked that page before, maybe there was a recent change, or maybe I just wasn't paying attention. 🤷

[JacquesCarette]

Could it be that @xplat has just solved this in PR #312 ?

[sstucki]

I wasn't following the discussions in #312. Could you point me to the relevant changes? I found this: https://github.com/xplat/agda-categories/blob/e34315c6c51abd78d9c35ac5d4774a09c07f0acb/src/Categories/Functor/Instance/ConnectedComponents.agda#L15-L16 but it says left-andjoit to Disc, whereas this issue is about Disc itself being left-andjoit to the forgetful functor from Cats to Set(oid)s.

TBH, I don't think the issue is finding suitable adjunctions (we've already mechanized several well-behaved candidates), but that the categories/functors involved aren't the "usual" ones. But I might be missing something.

[JacquesCarette]

Ah, I was probably reading too fast (yes, I meant that bit).