distinguish predicates and properties about agda-categories HOT 9 CLOSED

I'm not always fond of the IsX stuff. It would be especially odd in CT, where 'flat' theories seem to make sense. Having said that, I'm sure there are cases where the current setup is wrong, and should be fixed.

from agda-categories.

what do you mean? I suppose this is more like a stylistic issue, isn't it?

from agda-categories.

I don't like the IsMonoid structure that separates out all the properties into a bundle, with the rest 'unbundled'. It's a holdover from a combination of over-focusing on computation and downplaying proofs, and proof-irrelevance, which while not downplaying proofs as much, still says that there is no actual information content to proofs. This library is proof-relevant...

It is definitely a stylistic issue.

from agda-categories.

It is definitely a stylistic issue.

I guess that's true, but the reason why I mentioned this in #40 wasn't really stylistic. It was actually rather pragmatic. I was trying to implement the category Groupoidsof groupoids and functors, so I needed a structure Groupoid (of type Set o) for the objects. There was already a record Groupoid (in Categories.Category.Groupoid) but that wasn't the structure, it was a predicate on categories, the property of being a groupoid. Of course, I could have used Σ (Category _ _ _) Groupoid as the type of objects, but that's not very readable. I prefer to use records to give proper names to structures.

So my question is really: when there's a structure Ythat is an X with extra properties, and there are good reasons to both represent the structure Yand the property (predicate on Xs) of being a Y, how should the two be distinguished?

Note that I'm in no way suggesting that the predicate is somehow less important or that it has no information content. It simply has a different type, which I think should be reflected somehow in the name.

from agda-categories.

at this moment it is really done by repeating X. see for example:

indeed, if Monoidal were a structure instead of a predicate, this definition would look a bit more natural.

from agda-categories.

So I agree that, right now, Groupoid is ill-named, because it isn't the structure/type, but a predicate. I would be happy to change its name, and introduce a proper Groupoid.

Monoidal is to me different, because it adds additional structure on top of underlying structure. And you not infrequently want 2 monoidal structures on the same underlying category.

I guess I'd prefer to start with fixing the obvious cases that are wrong, and see what kind of naming convention emerges. I'm happy to release 0.X versions that are actively advertised as having a slightly unstable API -- and then ensure the 1.0 version stabilizes the core API. I don't feel like I quite know enough right now to suggest a naming convention that's going to be sufficiently future-proof.

from agda-categories.

The Groupoid issue has now been taken care of.
In most presentations of monoidal categories, it starts with "A Monoidal category is a category equipped with ...". So it does feel like it is naturally an over-structure; it definitely isn't a 'predicate'.
Interestingly, the one that I'm still most unsure of is Apex as part of Cone! In some of the uses, it would be better parametrized, and others like it is, as a structure. So I am quite undecided. [Or maybe it's the other way around, it's Cone that should be parametrized]

from agda-categories.

So things have definitely 'evolved' since this issue was created. We do have a bunch of IsX and also X. It does seem to work just fine.

The question is now: what's left to do to close this particular issue? There doesn't seem to be any active, outstanding items?

from agda-categories.

It's been a month since I asked about this, and no comments. Re-reading makes me think there's nothing left to do. At least, this issue won't caused any more direct work.

from agda-categories.