Challenge: prove that the Discrete functor is the (cartesian) left-adjoint of the forgetful functor from Cats to Sets about agda-categories HOT 8 OPEN

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

from agda-categories.

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.

from agda-categories.

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.

from agda-categories.

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.

from agda-categories.

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. 🤷

from agda-categories.

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

from agda-categories.

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.

from agda-categories.

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

from agda-categories.